Description: The successor of an ordinal number is an ordinal number. (Contributed by NM, 9-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | sucelon | ⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On ) |
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 ) |