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 )