$\newcommand{\set}[1]{\{#1\}}$ $\newcommand{\mr}{\mathscr}$ $\newcommand{\mc}{\mathcal}$ $\newcommand{\N}{\mathbb N}$
Definitions
Posets
Given to posets $P$ and $Q$, a map $f:P\to Q$ is called a poset map if $f(x)\leq f(y)$ whenever $x\leq y$. We say that $f$ is an embedding if $f$ is an injective poset map. We say that $f$ is an induced embedding if $f$ is an embedding with an additional property that $f(x)\not\leq f(y)$ whenever $x\not\leq y$. The idea is that $f(P)$ should be an `induced subposet' of $Q$.
Let $P$ be a poset. For $x, y\in P$ we say that $y$ covers $x$ if $x<y$ and there is no $z\in P$ such that $x<z<y$.
Graded Posets
A rank function on $P$ is a map $\rho:P\to \N$ such that $\rho(x)< \rho(y)$ whenever $x<y$ and $\rho(y) = \rho(x)+1$ whenever $y$ covers $x$.
A poset equipped with a rank function is called a graded poset. An example of a graded graded poset is the power set poset $\mc P(S)$ for any finite set $S$. The poset relation is given by inclusion and the rank of any element is the cardinality of that element. When $S$ is infinite, we write $\mc P_f(S)$ to denote the set of all the finite subsets of $S$. Clearly $\mc P_f(S)$ is also a graded poset with rank being cardinality.
Given graded posets $P$ and $Q$, a poset map $f:P\to Q$ is called graded if $\text{rank}(f(u)) = \text{rank}(f(v))$ whenever $\text{rank}(u) = \text{rank}(v)$.
Question
Question. Is is true that for every finite graded poset $P$ there is an induced graded embedding of $P$ into $\mc P_f(\N)$.
In other words, does every finite graded poset appear as a `graded induced subposet' of a large enough power set poset?
I think the answer to the above question is in the affirmative. I have supplied a proof below. I am not looking for a proof verification and only want to know if the statement is correct. In case the statement is indeed correct, if possible can you also provide a refernce? Thank you.
Purported Proof
For a graded poset $P$ we write $P_i$ to denote the set of all the elements of $P$ at level $i$.
Lemma 1. Let $P$ be a finite graded poset having $l+1$ levels, where $l$ is a positive integer. Let $f:P\to \mc P_f(\N)$ be an induced graded embedding. Let $X\sqcup Y$ be a partition of $P_l$ with $X$ non-empty. Then there is an induced graded embedding $\tilde f:P\to \mc P_f(\N)$ such that for any $y\in Y$ we have $\tilde f(y)$ is not contained in $\bigcup_{x\in X} f(x)$ (which is vacuously true if $Y$ is empty).
Proof. Let $S=\bigcup_{p\in P}f(p)$ and $n_0$ be a positive integer greater than $\max(S)$. Let $X=\set{x_1, \ldots, x_r}$, $Y=\set{y_1, \ldots, y_s}$, and $P_{l+1} = \set{a_1, \ldots, a_k}$. Define a map $\tilde f:P\to \mc P_f(\N)$ as $$ \tilde f(p) = f(p) \text{ if } p\in \bigcup_{j=1}^{l-1} P_{j}, $$ $$ \tilde f(x_i) = f(x_i) \cup \set{n_0 + i} \text{ for } 1\leq i\leq r, \quad \tilde f(y_j) = f(y_j) \cup \set{n_0+r+j} \text{ for } 1\leq j\leq s $$ and $$ \tilde f(a_i) = f(a_i) \cup \set{n_0+1, \ldots, n_0+r+s} \text{ for } 1\leq i\leq k $$ Now $\tilde f$ has the equired property. $\blacksquare$
Lemma 2. Let $P$ be a finite graded poset. Then there is an induced graded embedding of $P$ in $\mc P_f(\N)$.
Proof. We do this by induction on the number of levels of $P$. If $P$ has only one level then this is clear. So let $l\geq 1$ and assume that the lemma is proven for all graded posets having no more than $l$ levels. Let $P$ has $l+1$ levels. Write $P_i$ to denote the $i$-th level of $P$. Again, if $P_{l+1}$ is a singleton then one can easily extend a graded induced embedding of $P\setminus P_{l+1}$ in $\mc P_f(\N)$ (which exists by induction) to a graded induced embedding of $P_{l+1}$ in $\mc P_f(\N)$. So suppose there are $k+1$ elements in $P_{l+1}$ for some $k\geq 1$, and that the lemma holds whenever the size of the $(l+1)$-th level is smaller than $k+1$. Let $P_{l+1} = \set{a_1, \ldots, a_{k+1}}$. Let $X=\set{x_1, \ldots, x_r}$ be all the members of $P_l$ that are dominated by $a_{k+1}$ and $Y=\set{y_1, \ldots, y_s}$ be all the members of $P_l$ that are not dominated by $a_{k+1}$. Choose an induced graded embedding $f:P\setminus\set{a_{k+1}}\to \mc P_f(\N)$. Define $S=\bigcup_{p\in P}f(p)$.
Suppose $X$ is empty. Let $T\subseteq\N$ be set $\max S < \min T$. Define $f:P\to \mc P_f(\N)$ by declaring $g(p) = f(p)$ for all $p\in P\setminus \set{a_{k+1}}$ and set $g(a_{k+1}) = T$. Then $g$ is an induced graded embedding of $P$ in $\mc P_f(\N)$ and hence we may assume $X$ is non-empty.
Using Lemma 1we may assume that none of the $f(y_j)$'s is contained in $\bigcup_{x\in X} f(x)$. Let each $f(a_i)$ have size $\alpha$ and $\bigcup_{x\in X} f(x)$ have size $\beta$. Let $S=\bigcup_{p\in P,\ p\neq a_{k+1}}f(p)$ and let $U$ and $V$ be disjoint subsets of $\N$ such that $\max S< \min U, \min V$ such that $\alpha+|U| = \beta+|V|$. Define $g:P\to \mc P_f(\N)$ by declaring $g(p) = f(p)$ for all $p\in P_l$ and $$ g(a_i) = f(a_i) \cup V\text{ for } 1\leq i\leq k, \text{ and } g(a_{k+1}) = U\cup \bigcup_{x\in X} f(x) $$ Then $g$ has the required properties. $\blacksquare$
