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

Metamath Proof Explorer

Theorem sucon

Description: The class of all ordinal numbers is its own successor. (Contributed by NM, 12-Sep-2003)

Ref Expression
Assertion sucon 
|- suc On = On

Proof

Step Hyp Ref Expression
1 onprc 
 |-  -. On e. _V
2 sucprc 
 |-  ( -. On e. _V -> suc On = On )
3 1 2 ax-mp 
 |-  suc On = On