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

Metamath Proof Explorer

Theorem ordunisuc

Description: An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ordunisuc ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )

Proof

Step Hyp Ref Expression
1 ordeleqon ⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
2 suceq ⊢ ( 𝑥 = 𝐴 → suc 𝑥 = suc 𝐴 )
3 2 unieqd ⊢ ( 𝑥 = 𝐴 → ∪ suc 𝑥 = ∪ suc 𝐴 )
4 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
5 3 4 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ∪ suc 𝑥 = 𝑥 ↔ ∪ suc 𝐴 = 𝐴 ) )
6 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
7 ordtr ⊢ ( Ord 𝑥 → Tr 𝑥 )
8 6 7 syl ⊢ ( 𝑥 ∈ On → Tr 𝑥 )
9 vex ⊢ 𝑥 ∈ V
10 9 unisuc ⊢ ( Tr 𝑥 ↔ ∪ suc 𝑥 = 𝑥 )
11 8 10 sylib ⊢ ( 𝑥 ∈ On → ∪ suc 𝑥 = 𝑥 )
12 5 11 vtoclga ⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
13 sucon ⊢ suc On = On
14 13 unieqi ⊢ ∪ suc On = ∪ On
15 unon ⊢ ∪ On = On
16 14 15 eqtri ⊢ ∪ suc On = On
17 suceq ⊢ ( 𝐴 = On → suc 𝐴 = suc On )
18 17 unieqd ⊢ ( 𝐴 = On → ∪ suc 𝐴 = ∪ suc On )
19 id ⊢ ( 𝐴 = On → 𝐴 = On )
20 16 18 19 3eqtr4a ⊢ ( 𝐴 = On → ∪ suc 𝐴 = 𝐴 )
21 12 20 jaoi ⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ∪ suc 𝐴 = 𝐴 )
22 1 21 sylbi ⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )