This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴 ) )

Proof

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