Theorem suceloni

Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of TakeutiZaring p. 41. (Contributed by NM, 6-Jun-1994) (Proof shortened by BTernaryTau, 30-Nov-2024)

	Ref	Expression
Assertion	suceloni	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		sucexg	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ V )
2		sucexeloni	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ V ) → suc 𝐴 ∈ On )
3	1 2	mpdan	⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On )