Metamath Proof Explorer

Theorem sucelon

Description: The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003)

Ref Expression
Assertion sucelon 
|- ( A e. On <-> suc A e. On )

Proof

Step Hyp Ref Expression
1 ordsuc 
 |-  ( Ord A <-> Ord suc A )
2 sucexb 
 |-  ( A e. _V <-> suc A e. _V )
3 1 2 anbi12i 
 |-  ( ( Ord A /\ A e. _V ) <-> ( Ord suc A /\ suc A e. _V ) )
4 elon2 
 |-  ( A e. On <-> ( Ord A /\ A e. _V ) )
5 elon2 
 |-  ( suc A e. On <-> ( Ord suc A /\ suc A e. _V ) )
6 3 4 5 3bitr4i 
 |-  ( A e. On <-> suc A e. On )