Union of Set of Ordinals is Ordinal/Corollary
Corollary to Union of Set of Ordinals is Ordinal
Let $y$ be a set.
Let $\On$ be the class of all ordinals.
Let $F: y \to \On$ be a mapping.
Then:
- $\bigcup \map F y \in \On$
where $\map F y$ is the image of $y$ under $F$.
Proof 1
By the Axiom of Replacement, $\map F y$ is a set.
Thus by the Axiom of Unions, $\bigcup \map F y$ is a set.
By Union of Set of Ordinals is Ordinal, $\bigcup \map F y$ is transitive.
 | There is believed to be a mistake here, possibly a typo. In particular: This link is the result which needs to be proved. Something with transitive instead? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by reviewing it, and either correcting it or adding some explanatory material as to why you believe it is actually correct after all. 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 {{Mistake}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
By the epsilon relation $\bigcup \map F y$ is well-ordered.
 | This article, or a section of it, needs explaining. In particular: What does the above sentence mean? You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by explaining it. 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 {{Explain}} from the code. |
Thus $\bigcup \map F y$ is a member of $\On$, the class of all ordinals.
$\blacksquare$
Proof 2
| \(\ds x\) | \(\in\) | \(\ds \bigcup_{z \mathop \in y} \map F z\) | ||||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \exists z \in y: \, \) | \(\ds x\) | \(\in\) | \(\ds \map F z\) | Definition of Set Union | |||||||||
| \(\ds \leadsto \ \ \) | \(\ds x\) | \(\in\) | \(\ds \On\) | by hypothesis |
So:
- $\ds \bigcup_{z \mathop \in y} \map F z \subseteq \On$
| \(\ds x\) | \(\in\) | \(\ds \bigcup_{z \mathop \in y} \map F z\) | ||||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \exists z \in y: \, \) | \(\ds x\) | \(\in\) | \(\ds \map F z\) | Definition of Set Union | |||||||||
| \(\ds \leadsto \ \ \) | \(\ds \exists z \in y: \, \) | \(\ds x\) | \(\subseteq\) | \(\ds \map F z\) | Ordinal is Transitive | |||||||||
| \(\ds \leadsto \ \ \) | \(\ds x\) | \(\subseteq\) | \(\ds \bigcup_{z \mathop \in y} \map F z\) | Union Preserved Under Subset Relation |
So $\ds \bigcup_{z \mathop \in y} \map F z$ is a transitive set.
Therefore $\ds \bigcup_{z \mathop \in y} \map F z$ is an ordinal.
- $\ds \bigcup_{z \mathop \in y} \map F z = \bigcup \Img y$
Let $U$ denote the universal class.
| \(\ds y\) | \(\in\) | \(\ds V\) | ||||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \bigcup \Img y\) | \(\in\) | \(\ds V\) | Axiom of Replacement Equivalents | ||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \bigcup \bigcup \Img y\) | \(\in\) | \(\ds V\) | Axiom of Unions Equivalents | ||||||||||
| \(\ds \leadsto \ \ \) | \(\ds \bigcup_{z \mathop \in y} \map F z\) | \(\in\) | \(\ds V\) | Equality given above |
Therefore $\ds \bigcup_{z \mathop \in y} \map F z$ is a set, so it is a member of the class of all ordinals.
$\blacksquare$