Metamath Proof Explorer


Theorem ordsuc

Description: A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995) Avoid ax-un . (Revised by BTernaryTau, 6-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 ordsuci ( Ord 𝐴 → Ord suc 𝐴 )
2 sucidg ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 )
3 ordelord ( ( Ord suc 𝐴𝐴 ∈ suc 𝐴 ) → Ord 𝐴 )
4 3 ex ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) )
5 2 4 syl5com ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
6 sucprc ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )
7 6 eqcomd ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 )
8 ordeq ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
9 7 8 syl ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) )
10 9 biimprd ( ¬ 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) )
11 5 10 pm2.61i ( Ord suc 𝐴 → Ord 𝐴 )
12 1 11 impbii ( Ord 𝐴 ↔ Ord suc 𝐴 )