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

Proof

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