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	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2		ordsuci	⊢ ( Ord 𝐴 → Ord suc 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ On → Ord suc 𝐴 )
4		elex	⊢ ( suc 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V )
5		elong	⊢ ( suc 𝐴 ∈ V → ( suc 𝐴 ∈ On ↔ Ord suc 𝐴 ) )
6	5	biimparc	⊢ ( ( Ord suc 𝐴 ∧ suc 𝐴 ∈ V ) → suc 𝐴 ∈ On )
7	3 4 6	syl2an	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )