Metamath Proof Explorer

Theorem ordzsl

Description: An ordinal is zero, a successor ordinal, or a limit ordinal. (Contributed by NM, 1-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 orduninsuc ⊢ Ord ⁡ A → A = ⋃ A ↔ ¬ ∃ x ∈ On A = suc ⁡ x
2 1 biimprd ⊢ Ord ⁡ A → ¬ ∃ x ∈ On A = suc ⁡ x → A = ⋃ A
3 unizlim ⊢ Ord ⁡ A → A = ⋃ A ↔ A = ∅ ∨ Lim ⁡ A
4 2 3 sylibd ⊢ Ord ⁡ A → ¬ ∃ x ∈ On A = suc ⁡ x → A = ∅ ∨ Lim ⁡ A
5 4 orrd ⊢ Ord ⁡ A → ∃ x ∈ On A = suc ⁡ x ∨ A = ∅ ∨ Lim ⁡ A
6 3orass ⊢ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A
7 or12 ⊢ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A ↔ ∃ x ∈ On A = suc ⁡ x ∨ A = ∅ ∨ Lim ⁡ A
8 6 7 bitri ⊢ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A ↔ ∃ x ∈ On A = suc ⁡ x ∨ A = ∅ ∨ Lim ⁡ A
9 5 8 sylibr ⊢ Ord ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A
10 ord0 ⊢ Ord ⁡ ∅
11 ordeq ⊢ A = ∅ → Ord ⁡ A ↔ Ord ⁡ ∅
12 10 11 mpbiri ⊢ A = ∅ → Ord ⁡ A
13 suceloni ⊢ x ∈ On → suc ⁡ x ∈ On
14 eleq1 ⊢ A = suc ⁡ x → A ∈ On ↔ suc ⁡ x ∈ On
15 13 14 syl5ibr ⊢ 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 ∈ On A = suc ⁡ x → Ord ⁡ A
19 limord ⊢ Lim ⁡ A → Ord ⁡ A
20 12 18 19 3jaoi ⊢ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A → Ord ⁡ A
21 9 20 impbii ⊢ Ord ⁡ A ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A