Theorem ordsuc 7806

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

Assertion

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

Proof of Theorem ordsuc

Step	Hyp	Ref	Expression
1		ordsuci 7803	. 2 ⊢ (Ord 𝐴 → Ord suc 𝐴)
2		sucidg 6442	. . . 4 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3		ordelord 6380	. . . . 5 ⊢ ((Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴) → Ord 𝐴)
4	3	ex 417	. . . 4 ⊢ (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
5	2, 4	syl5com 32	. . 3 ⊢ (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6		sucprc 6437	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → suc 𝐴 = 𝐴)
7	6	eqcomd 2775	. . . . 5 ⊢ (¬ 𝐴 ∈ V → 𝐴 = suc 𝐴)
8		ordeq 6365	. . . . 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 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149  Vcvv 3463  Ord word 6357  suc csuc 6360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-tr 5220  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6361  df-on 6362  df-suc 6364

This theorem is referenced by:  ordpwsuc  7807  onsucb  7809  ordsucss  7810  onpsssuc  7811  ordsucelsuc  7814  ordsucsssuc  7815  ordsucuniel  7816  ordsucun  7817  onsucuni2  7826  0elsuc  7827  nlimsucg  7834  limsssuc  7842  cofon1  8654  cofon2  8655  php4  9190  cantnflt  9637  fin23lem26  10305  hsmexlem1  10406  nosupres  27833  noetasuplem4  27862  noetainflem4  27866  cutbdaybnd2lim  27952  satfn  35742  onsuct0  36837  ordsssucim  44016  dfsucon  44136