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 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ 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		suceloni	⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
14		eleq1	⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ∈ On ↔ suc 𝑥 ∈ On ) )
15	13 14	syl5ibr	⊢ ( 𝐴 = 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 𝐴 ) )