Theorem sucexeloni

Description: If the successor of an ordinal number exists, it is an ordinal number. This variation of onsuc does not require ax-un . (Contributed by BTernaryTau, 30-Nov-2024) (Proof shortened by BJ, 11-Jan-2025)

	Ref	Expression
Assertion	sucexeloni	|- ( ( A e. On /\ suc A e. V ) -> suc A e. On )

Proof

Step	Hyp	Ref	Expression
1		eloni	|- ( A e. On -> Ord A )
2		ordsuci	|- ( Ord A -> Ord suc A )
3	1 2	syl	|- ( A e. On -> Ord suc A )
4		elex	|- ( suc A e. V -> suc A e. _V )
5		elong	|- ( suc A e. _V -> ( suc A e. On <-> Ord suc A ) )
6	5	biimparc	|- ( ( Ord suc A /\ suc A e. _V ) -> suc A e. On )
7	3 4 6	syl2an	|- ( ( A e. On /\ suc A e. V ) -> suc A e. On )