Metamath Proof Explorer

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 \in On \land suc A \in V) \to suc A \in On$

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		ordsuci	$⊢ Ord A \to Ord suc A$
3	1 2	syl	$⊢ A \in On \to Ord suc A$
4		elex	$⊢ suc A \in V \to suc A \in V$
5		elong	$⊢ suc A \in V \to (suc A \in On \leftrightarrow Ord suc A)$
6	5	biimparc	$⊢ (Ord suc A \land suc A \in V) \to suc A \in On$
7	3 4 6	syl2an	$⊢ (A \in On \land suc A \in V) \to suc A \in On$