Metamath Proof Explorer

Theorem onsucuni3

Description: If an ordinal number has a predecessor, then it is successor of that predecessor. (Contributed by ML, 17-Oct-2020)

Ref Expression
Assertion onsucuni3 ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → B = suc ⁡ ⋃ B

Proof

Step Hyp Ref Expression
1 eloni ⊢ B ∈ On → Ord ⁡ B
2 1 3ad2ant1 ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → Ord ⁡ B
3 orduniorsuc ⊢ Ord ⁡ B → B = ⋃ B ∨ B = suc ⁡ ⋃ B
4 2 3 syl ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → B = ⋃ B ∨ B = suc ⁡ ⋃ B
5 4 orcomd ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → B = suc ⁡ ⋃ B ∨ B = ⋃ B
6 simp2 ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → B ≠ ∅
7 df-lim ⊢ Lim ⁡ B ↔ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B
8 7 biimpri ⊢ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B → Lim ⁡ B
9 8 3expb ⊢ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B → Lim ⁡ B
10 9 con3i ⊢ ¬ Lim ⁡ B → ¬ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B
11 10 3ad2ant3 ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → ¬ Ord ⁡ B ∧ B ≠ ∅ ∧ B = ⋃ B
12 2 11 mpnanrd ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → ¬ B ≠ ∅ ∧ B = ⋃ B
13 6 12 mpnanrd ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → ¬ B = ⋃ B
14 orcom ⊢ B = suc ⁡ ⋃ B ∨ B = ⋃ B ↔ B = ⋃ B ∨ B = suc ⁡ ⋃ B
15 df-or ⊢ B = ⋃ B ∨ B = suc ⁡ ⋃ B ↔ ¬ B = ⋃ B → B = suc ⁡ ⋃ B
16 14 15 sylbb ⊢ B = suc ⁡ ⋃ B ∨ B = ⋃ B → ¬ B = ⋃ B → B = suc ⁡ ⋃ B
17 5 13 16 sylc ⊢ B ∈ On ∧ B ≠ ∅ ∧ ¬ Lim ⁡ B → B = suc ⁡ ⋃ B