Metamath Proof Explorer


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 )