Theorem ordsuc 7827

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

Assertion

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

Proof of Theorem ordsuc

Step	Hyp	Ref	Expression
1		ordsuci 7824	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6448	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6386	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
4	3	ex 418	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
5	2, 4	syl5com 32	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6		sucprc 6443	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2766	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6371	. . . . 5 ⊢ (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
9	7, 8	syl 18	. . . 4 ⊢ (¬ 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
10	9	biimprd 251	. . 3 ⊢ (¬ 𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
11	5, 10	pm2.61i 184	. 2 ⊢ (Ord suc 𝐴 → Ord 𝐴)
12	1, 11	impbii 212	1 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  Vcvv 3450  Ord word 6363  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6367  df-on 6368  df-suc 6370

This theorem is used by:  ordpwsuc  7828  onsucb  7830  ordsucss  7831  onpsssuc  7832  ordsucelsuc  7835  ordsucsssuc  7836  ordsucuniel  7837  ordsucun  7838  onsucuni2  7847  0elsuc  7848  nlimsucg  7855  limsssuc  7863  cofon1  8686  cofon2  8687  php4  9230  cantnflt  9678  fin23lem26  10408  hsmexlem1  10509  nosupres  28071  noetasuplem4  28100  noetainflem4  28104  cutbdaybnd2lim  28190  satfn  36208  onsuct0  37323  ordsssucim  44511  dfsucon  44631