Draft:Union of Set of Sets is Greatest Element under Subset Relation

Tule-hog suggests: The validity of the material on this page is questionable. In particular: immediate use case for this proof is part of Set with Choice Function is Well-Orderable (in particular, at Union of g-Tower is Greatest Element and Unique Fixed Point), which is based in Smullyan and Fitting's class theory. however, the argument cites ZFC. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by resolving the issues. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Questionable}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

Theorem

Let $M$ be a set.

Let $\bigcup M \in M$.

Let $(M, \subseteq)$ be the ordered set formed on $M$ by the subset relation (see Subset Relation is Ordering).

Then $\bigcup M$ is the greatest set by set inclusion ($M$ corresponds to $\TT$) of $(M, \subseteq)$.

Proof

By Set is Subset of Union:

$\forall \paren {N \in M}: N \subseteq \bigcup M$.

Therefore, $\bigcup M$ is the greatest element under the subset relation.

$\blacksquare$