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 ⁡ A ↔ Ord ⁡ suc ⁡ A

Proof

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