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	⊢ ( Ord 𝐴 → ∪ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) }
2		incom	⊢ ( { 𝑥 ∣ 𝑥 ∈ On } ∩ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ) = ( { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ∩ { 𝑥 ∣ 𝑥 ∈ On } )
3		inab	⊢ ( { 𝑥 ∣ 𝑥 ∈ On } ∩ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ) = { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) }
4		df-pw	⊢ 𝒫 𝐴 = { 𝑥 ∣ 𝑥 ⊆ 𝐴 }
5	4	eqcomi	⊢ { 𝑥 ∣ 𝑥 ⊆ 𝐴 } = 𝒫 𝐴
6		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ On } = On
7	5 6	ineq12i	⊢ ( { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ∩ { 𝑥 ∣ 𝑥 ∈ On } ) = ( 𝒫 𝐴 ∩ On )
8	2 3 7	3eqtr3i	⊢ { 𝑥 ∣ ( 𝑥 ∈ On ∧ 𝑥 ⊆ 𝐴 ) } = ( 𝒫 𝐴 ∩ On )
9	1 8	eqtri	⊢ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = ( 𝒫 𝐴 ∩ On )
10		ordpwsuc	⊢ ( Ord 𝐴 → ( 𝒫 𝐴 ∩ On ) = suc 𝐴 )
11	9 10	syl5eq	⊢ ( Ord 𝐴 → { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = suc 𝐴 )
12	11	unieqd	⊢ ( Ord 𝐴 → ∪ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = ∪ suc 𝐴 )
13		ordunisuc	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
14	12 13	eqtrd	⊢ ( Ord 𝐴 → ∪ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )