This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( Ord 𝐴 → { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = suc 𝐴 )
12 11 unieqd ⊢ ( Ord 𝐴 → ∪ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = ∪ suc 𝐴 )
13 ordunisuc ⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
14 12 13 eqtrd ⊢ ( Ord 𝐴 → ∪ { 𝑥 ∈ On ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )