Theorem orduniss2

Description: The union of the ordinal subsets of an ordinal number is that number. (Contributed by NM, 30-Jan-2005)

	Ref	Expression
Assertion	orduniss2	$$⊢\mathrm{Ord}A\to \bigcup \left\{x\in \mathrm{On}|x\subseteq A\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in \mathrm{On}|x\subseteq A\right\}=\left\{x|\left(x\in \mathrm{On}\wedge x\subseteq A\right)\right\}$$
2		incom	$$⊢\left\{x|x\in \mathrm{On}\right\}\cap \left\{x|x\subseteq A\right\}=\left\{x|x\subseteq A\right\}\cap \left\{x|x\in \mathrm{On}\right\}$$
3		inab	$$⊢\left\{x|x\in \mathrm{On}\right\}\cap \left\{x|x\subseteq A\right\}=\left\{x|\left(x\in \mathrm{On}\wedge x\subseteq A\right)\right\}$$
4		df-pw	$$⊢𝒫A=\left\{x|x\subseteq A\right\}$$
5	4	eqcomi	$$⊢\left\{x|x\subseteq A\right\}=𝒫A$$
6		abid2	$$⊢\left\{x|x\in \mathrm{On}\right\}=\mathrm{On}$$
7	5 6	ineq12i	$$⊢\left\{x|x\subseteq A\right\}\cap \left\{x|x\in \mathrm{On}\right\}=𝒫A\cap \mathrm{On}$$
8	2 3 7	3eqtr3i	$$⊢\left\{x|\left(x\in \mathrm{On}\wedge x\subseteq A\right)\right\}=𝒫A\cap \mathrm{On}$$
9	1 8	eqtri	$$⊢\left\{x\in \mathrm{On}|x\subseteq A\right\}=𝒫A\cap \mathrm{On}$$
10		ordpwsuc	$$⊢\mathrm{Ord}A\to 𝒫A\cap \mathrm{On}=\mathrm{suc}A$$
11	9 10	syl5eq	$$⊢\mathrm{Ord}A\to \left\{x\in \mathrm{On}|x\subseteq A\right\}=\mathrm{suc}A$$
12	11	unieqd	$$⊢\mathrm{Ord}A\to \bigcup \left\{x\in \mathrm{On}|x\subseteq A\right\}=\bigcup \mathrm{suc}A$$
13		ordunisuc	$$⊢\mathrm{Ord}A\to \bigcup \mathrm{suc}A=A$$
14	12 13	eqtrd	$$⊢\mathrm{Ord}A\to \bigcup \left\{x\in \mathrm{On}|x\subseteq A\right\}=A$$