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