Metamath Proof Explorer

Theorem ordzsl

Description: An ordinal is zero, a successor ordinal, or a limit ordinal. Remark 1.12 of Schloeder p. 2. (Contributed by NM, 1-Oct-2003)

Ref Expression
Assertion ordzsl ⊢Ord⁡A↔A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A

Proof

Step Hyp Ref Expression
1 orduninsuc ⊢Ord⁡A→A=⋃A↔¬∃x∈OnA=suc⁡x
2 1 biimprd ⊢Ord⁡A→¬∃x∈OnA=suc⁡x→A=⋃A
3 unizlim ⊢Ord⁡A→A=⋃A↔A=∅∨Lim⁡A
4 2 3 sylibd ⊢Ord⁡A→¬∃x∈OnA=suc⁡x→A=∅∨Lim⁡A
5 4 orrd ⊢Ord⁡A→∃x∈OnA=suc⁡x∨A=∅∨Lim⁡A
6 3orass ⊢A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A↔A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A
7 or12 ⊢A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A↔∃x∈OnA=suc⁡x∨A=∅∨Lim⁡A
8 6 7 bitri ⊢A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A↔∃x∈OnA=suc⁡x∨A=∅∨Lim⁡A
9 5 8 sylibr ⊢Ord⁡A→A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A
10 ord0 ⊢Ord⁡∅
11 ordeq ⊢A=∅→Ord⁡A↔Ord⁡∅
12 10 11 mpbiri ⊢A=∅→Ord⁡A
13 onsuc ⊢x∈On→suc⁡x∈On
14 eleq1 ⊢A=suc⁡x→A∈On↔suc⁡x∈On
15 13 14 imbitrrid ⊢A=suc⁡x→x∈On→A∈On
16 eloni ⊢A∈On→Ord⁡A
17 15 16 syl6com ⊢x∈On→A=suc⁡x→Ord⁡A
18 17 rexlimiv ⊢∃x∈OnA=suc⁡x→Ord⁡A
19 limord ⊢Lim⁡A→Ord⁡A
20 12 18 19 3jaoi ⊢A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A→Ord⁡A
21 9 20 impbii ⊢Ord⁡A↔A=∅∨∃x∈OnA=suc⁡x∨Lim⁡A