Metamath Proof Explorer

Theorem onzsl

Description: An ordinal number is zero, a successor ordinal, or a limit ordinal number. (Contributed by NM, 1-Oct-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion onzsl ⊢ A ∈ On ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ On → A ∈ V
2 eloni ⊢ A ∈ On → Ord ⁡ A
3 ordzsl ⊢ Ord ⁡ A ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A
4 3mix1 ⊢ A = ∅ → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
5 4 adantl ⊢ A ∈ V ∧ A = ∅ → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
6 3mix2 ⊢ ∃ x ∈ On A = suc ⁡ x → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
7 6 adantl ⊢ A ∈ V ∧ ∃ x ∈ On A = suc ⁡ x → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
8 3mix3 ⊢ A ∈ V ∧ Lim ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
9 5 7 8 3jaodan ⊢ A ∈ V ∧ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ Lim ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
10 3 9 sylan2b ⊢ A ∈ V ∧ Ord ⁡ A → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
11 1 2 10 syl2anc ⊢ A ∈ On → A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A
12 0elon ⊢ ∅ ∈ On
13 eleq1 ⊢ A = ∅ → A ∈ On ↔ ∅ ∈ On
14 12 13 mpbiri ⊢ A = ∅ → A ∈ On
15 suceloni ⊢ x ∈ On → suc ⁡ x ∈ On
16 eleq1 ⊢ A = suc ⁡ x → A ∈ On ↔ suc ⁡ x ∈ On
17 15 16 syl5ibrcom ⊢ x ∈ On → A = suc ⁡ x → A ∈ On
18 17 rexlimiv ⊢ ∃ x ∈ On A = suc ⁡ x → A ∈ On
19 limelon ⊢ A ∈ V ∧ Lim ⁡ A → A ∈ On
20 14 18 19 3jaoi ⊢ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A → A ∈ On
21 11 20 impbii ⊢ A ∈ On ↔ A = ∅ ∨ ∃ x ∈ On A = suc ⁡ x ∨ A ∈ V ∧ Lim ⁡ A