Does every finite graded poset appear as a graded induced subposet of the power-set poset? $\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$
 A: Apoligize If I have missed a point, it feels like I might have read it too fast, but here are my 2 cents.
A note on your proof : it seems to me that in the lemma 1 you assume the existence of an induced graded embedding $f:P\to\mathcal{P}_f(\mathbb{N})$, and then in lemma 2 you use lemma 1 to prove its existence. Isn't it redundant?
Regarding the original question. My guess would be no. My main reason for that is Birkhoff's representation theorem.

Every distributive lattice can be embedded in some sufficiently large boolean lattice

Meaning that you need additional requirement on your poset $P$ for the result to hold :

*

*it has to be a lattice : for every pair of elements $x,y \in P$, the $\sup$ and $\inf$ functions are well-defined:
$$ \sup(x,y)=x\vee y : \text{smallest elements $z$ such that $x\leq z$ and $y\leq z$}$$
$$ \inf(x,y)=x\wedge y : \text{largest elements $z$ such that $x\geq z$ and $y\geq z$}$$

*it has to be distributive : for every elements $x,y,z\in P$
$$ x\wedge(y\vee z) = (x\wedge y)\vee (x\wedge z)$$
Then for these posets the results hold by Birkhoff theorem.
If you build a poset that is not a lattice, for example including two elements $x,y$, for which the $\sup$ is not well-defined, i.e. having the same two immediate cover $z_1$ and $z_2$,

Then I don't think you can find an induced embedding into $\mathcal{P}(\mathbb{N})$.
