MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordsuc Structured version   Visualization version   GIF version

Theorem ordsuc 7797
Description: A class is ordinal if and only if its successor is ordinal. (Contributed by NM, 3-Apr-1995.) Avoid ax-un 7721. (Revised by BTernaryTau, 6-Jan-2025.)
Assertion
Ref Expression
ordsuc (Ord 𝐴 ↔ Ord suc 𝐴)

Proof of Theorem ordsuc
StepHypRef Expression
1 ordsuci 7792 . 2 (Ord 𝐴 → Ord suc 𝐴)
2 sucidg 6442 . . . 4 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3 ordelord 6383 . . . . 5 ((Ord suc 𝐴𝐴 ∈ suc 𝐴) → Ord 𝐴)
43ex 413 . . . 4 (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
52, 4syl5com 31 . . 3 (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6 sucprc 6437 . . . . . 6 𝐴 ∈ V → suc 𝐴 = 𝐴)
76eqcomd 2738 . . . . 5 𝐴 ∈ V → 𝐴 = suc 𝐴)
8 ordeq 6368 . . . . 5 (𝐴 = suc 𝐴 → (Ord 𝐴 ↔ Ord suc 𝐴))
97, 8syl 17 . . . 4 𝐴 ∈ V → (Ord 𝐴 ↔ Ord suc 𝐴))
109biimprd 247 . . 3 𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
115, 10pm2.61i 182 . 2 (Ord suc 𝐴 → Ord 𝐴)
121, 11impbii 208 1 (Ord 𝐴 ↔ Ord suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1541  wcel 2106  Vcvv 3474  Ord word 6360  suc csuc 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-ord 6364  df-on 6365  df-suc 6367
This theorem is referenced by:  ordpwsuc  7799  onsucb  7801  ordsucss  7802  onpsssuc  7803  ordsucelsuc  7806  ordsucsssuc  7807  ordsucuniel  7808  ordsucun  7809  onsucuni2  7818  0elsuc  7819  nlimsucg  7827  limsssuc  7835  cofon1  8667  cofon2  8668  php4  9209  cantnflt  9663  fin23lem26  10316  hsmexlem1  10417  nosupres  27199  noetasuplem4  27228  noetainflem4  27232  scutbdaybnd2lim  27307  satfn  34334  onsuct0  35314  ordsssucim  42138  dfsucon  42259
  Copyright terms: Public domain W3C validator