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

Metamath Proof Explorer

Theorem ordsuc

Description: A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995) Avoid ax-un . (Revised by BTernaryTau, 6-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 ordsuci 
 |-  ( Ord A -> Ord suc A )
2 sucidg 
 |-  ( A e. _V -> A e. suc A )
3 ordelord 
 |-  ( ( Ord suc A /\ A e. suc A ) -> Ord A )
4 3 ex 
 |-  ( Ord suc A -> ( A e. suc A -> Ord A ) )
5 2 4 syl5com 
 |-  ( A e. _V -> ( Ord suc A -> Ord A ) )
6 sucprc 
 |-  ( -. A e. _V -> suc A = A )
7 6 eqcomd 
 |-  ( -. A e. _V -> A = suc A )
8 ordeq 
 |-  ( A = suc A -> ( Ord A <-> Ord suc A ) )
9 7 8 syl 
 |-  ( -. A e. _V -> ( Ord A <-> Ord suc A ) )
10 9 biimprd 
 |-  ( -. A e. _V -> ( Ord suc A -> Ord A ) )
11 5 10 pm2.61i 
 |-  ( Ord suc A -> Ord A )
12 1 11 impbii 
 |-  ( Ord A <-> Ord suc A )