Theorem sucelon

Description: The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003)

	Ref	Expression
Assertion	sucelon	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		ordsuc	⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 )
2		sucexb	⊢ ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V )
3	1 2	anbi12i	⊢ ( ( Ord 𝐴 ∧ 𝐴 ∈ V ) ↔ ( Ord suc 𝐴 ∧ suc 𝐴 ∈ V ) )
4		elon2	⊢ ( 𝐴 ∈ On ↔ ( Ord 𝐴 ∧ 𝐴 ∈ V ) )
5		elon2	⊢ ( suc 𝐴 ∈ On ↔ ( Ord suc 𝐴 ∧ suc 𝐴 ∈ V ) )
6	3 4 5	3bitr4i	⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On )