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

Metamath Proof Explorer

Theorem onsucuni2

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

Ref Expression
Assertion onsucuni2 ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = 𝐴 )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝐴 = suc 𝐵 → ( 𝐴 ∈ On ↔ suc 𝐵 ∈ On ) )
2 1 biimpac ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc 𝐵 ∈ On )
3 eloni ⊢ ( suc 𝐵 ∈ On → Ord suc 𝐵 )
4 ordsuc ⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
5 ordunisuc ⊢ ( Ord 𝐵 → ∪ suc 𝐵 = 𝐵 )
6 4 5 sylbir ⊢ ( Ord suc 𝐵 → ∪ suc 𝐵 = 𝐵 )
7 suceq ⊢ ( ∪ suc 𝐵 = 𝐵 → suc ∪ suc 𝐵 = suc 𝐵 )
8 6 7 syl ⊢ ( Ord suc 𝐵 → suc ∪ suc 𝐵 = suc 𝐵 )
9 ordunisuc ⊢ ( Ord suc 𝐵 → ∪ suc suc 𝐵 = suc 𝐵 )
10 8 9 eqtr4d ⊢ ( Ord suc 𝐵 → suc ∪ suc 𝐵 = ∪ suc suc 𝐵 )
11 2 3 10 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ suc 𝐵 = ∪ suc suc 𝐵 )
12 unieq ⊢ ( 𝐴 = suc 𝐵 → ∪ 𝐴 = ∪ suc 𝐵 )
13 suceq ⊢ ( ∪ 𝐴 = ∪ suc 𝐵 → suc ∪ 𝐴 = suc ∪ suc 𝐵 )
14 12 13 syl ⊢ ( 𝐴 = suc 𝐵 → suc ∪ 𝐴 = suc ∪ suc 𝐵 )
15 suceq ⊢ ( 𝐴 = suc 𝐵 → suc 𝐴 = suc suc 𝐵 )
16 15 unieqd ⊢ ( 𝐴 = suc 𝐵 → ∪ suc 𝐴 = ∪ suc suc 𝐵 )
17 14 16 eqeq12d ⊢ ( 𝐴 = suc 𝐵 → ( suc ∪ 𝐴 = ∪ suc 𝐴 ↔ suc ∪ suc 𝐵 = ∪ suc suc 𝐵 ) )
18 11 17 imbitrrid ⊢ ( 𝐴 = suc 𝐵 → ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = ∪ suc 𝐴 ) )
19 18 anabsi7 ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = ∪ suc 𝐴 )
20 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
21 ordunisuc ⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
22 20 21 syl ⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
23 22 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → ∪ suc 𝐴 = 𝐴 )
24 19 23 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = 𝐴 )