Metamath Proof Explorer

Theorem ordsuc

Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995)

Ref Expression
Assertion ordsuc 
|- ( Ord A <-> Ord suc A )

Proof

Step Hyp Ref Expression
1 elong 
 |-  ( A e. _V -> ( A e. On <-> Ord A ) )
2 suceloni 
 |-  ( A e. On -> suc A e. On )
3 eloni 
 |-  ( suc A e. On -> Ord suc A )
4 2 3 syl 
 |-  ( A e. On -> Ord suc A )
5 1 4 syl6bir 
 |-  ( A e. _V -> ( Ord A -> Ord suc A ) )
6 sucidg 
 |-  ( A e. _V -> A e. suc A )
7 ordelord 
 |-  ( ( Ord suc A /\ A e. suc A ) -> Ord A )
8 7 ex 
 |-  ( Ord suc A -> ( A e. suc A -> Ord A ) )
9 6 8 syl5com 
 |-  ( A e. _V -> ( Ord suc A -> Ord A ) )
10 5 9 impbid 
 |-  ( A e. _V -> ( Ord A <-> Ord suc A ) )
11 sucprc 
 |-  ( -. A e. _V -> suc A = A )
12 11 eqcomd 
 |-  ( -. A e. _V -> A = suc A )
13 ordeq 
 |-  ( A = suc A -> ( Ord A <-> Ord suc A ) )
14 12 13 syl 
 |-  ( -. A e. _V -> ( Ord A <-> Ord suc A ) )
15 10 14 pm2.61i 
 |-  ( Ord A <-> Ord suc A )