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	$⊢ Ord A \to ⋃ \{x \in On \| x \subseteq A\} = A$

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

Metamath Proof Explorer