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 ⊢ A ∈ On ∧ A = suc ⁡ B → suc ⁡ ⋃ A = A

Proof

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