Metamath Proof Explorer


Theorem ordsuc

Description: The successor of an ordinal class is ordinal. (Contributed by NM, 3-Apr-1995)

Ref Expression
Assertion ordsuc ( Ord 𝐴 ↔ Ord suc 𝐴 )

Proof

Step Hyp Ref Expression
1 elong ( 𝐴 ∈ V → ( 𝐴 ∈ On ↔ Ord 𝐴 ) )
2 suceloni ( 𝐴 ∈ On → suc 𝐴 ∈ On )
3 eloni ( suc 𝐴 ∈ On → Ord suc 𝐴 )
4 2 3 syl ( 𝐴 ∈ On → Ord suc 𝐴 )
5 1 4 syl6bir ( 𝐴 ∈ V → ( Ord 𝐴 → Ord suc 𝐴 ) )
6 sucidg ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
7 ordelord ( ( Ord suc 𝐴𝐴 ∈ suc 𝐴 ) → Ord 𝐴 )
8 7 ex ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) )
9 6 8 syl5com ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
10 5 9 impbid ( 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
11 sucprc ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )
12 11 eqcomd ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 )
13 ordeq ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
14 12 13 syl ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
15 10 14 pm2.61i ( Ord 𝐴 ↔ Ord suc 𝐴 )