Under which name is the following proposition filed actually:
Every poset $P$ embeds fully and faithfully in the powerset of $P$, ordered by subset inclusion.
Let me call it Dedekind's lemma. Next to Cayley's theorem:
Every group $G$ is isomorphic to a subgroup of the symmetric group acting on $G$.
it is a prominent special case of Yoneda's lemma.
All proofs are constructive, and so is the proof of Erdös' lemma on intersection graphs:
Every graph $G$ is isomorphic to a family of subsets $S_i$ of a set S such that $v_i$ and $v_j$ are joined by an edge iff $S_i \cap S_j \neq \emptyset$
What I wonder about is:
Is Erdös' lemma on intersection graphs a special case of Yoneda's lemma?