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 = (/) \/ E. x e. On A = suc x \/ Lim A ) )

Proof

Step Hyp Ref Expression
1 orduninsuc 
 |-  ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )
2 1 biimprd 
 |-  ( Ord A -> ( -. E. x e. On A = suc x -> A = U. A ) )
3 unizlim 
 |-  ( Ord A -> ( A = U. A <-> ( A = (/) \/ Lim A ) ) )
4 2 3 sylibd 
 |-  ( Ord A -> ( -. E. x e. On A = suc x -> ( A = (/) \/ Lim A ) ) )
5 4 orrd 
 |-  ( Ord A -> ( E. x e. On A = suc x \/ ( A = (/) \/ Lim A ) ) )
6 3orass 
 |-  ( ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) <-> ( A = (/) \/ ( E. x e. On A = suc x \/ Lim A ) ) )
7 or12 
 |-  ( ( A = (/) \/ ( E. x e. On A = suc x \/ Lim A ) ) <-> ( E. x e. On A = suc x \/ ( A = (/) \/ Lim A ) ) )
8 6 7 bitri 
 |-  ( ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) <-> ( E. x e. On A = suc x \/ ( A = (/) \/ Lim A ) ) )
9 5 8 sylibr 
 |-  ( Ord A -> ( A = (/) \/ E. x e. 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 e. On -> suc x e. On )
14 eleq1 
 |-  ( A = suc x -> ( A e. On <-> suc x e. On ) )
15 13 14 syl5ibr 
 |-  ( A = suc x -> ( x e. On -> A e. On ) )
16 eloni 
 |-  ( A e. On -> Ord A )
17 15 16 syl6com 
 |-  ( x e. On -> ( A = suc x -> Ord A ) )
18 17 rexlimiv 
 |-  ( E. x e. On A = suc x -> Ord A )
19 limord 
 |-  ( Lim A -> Ord A )
20 12 18 19 3jaoi 
 |-  ( ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) -> Ord A )
21 9 20 impbii 
 |-  ( Ord A <-> ( A = (/) \/ E. x e. On A = suc x \/ Lim A ) )