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

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

Proof of Theorem ordsuc
StepHypRef Expression
1 ordsuci 7742 . 2 (Ord 𝐴 → Ord suc 𝐴)
2 sucidg 6398 . . . 4 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3 ordelord 6339 . . . . 5 ((Ord suc 𝐴𝐴 ∈ suc 𝐴) → Ord 𝐴)
43ex 413 . . . 4 (Ord suc 𝐴 → (𝐴 ∈ suc 𝐴 → Ord 𝐴))
52, 4syl5com 31 . . 3 (𝐴 ∈ V → (Ord suc 𝐴 → Ord 𝐴))
6 sucprc 6393 . . . . . 6 𝐴 ∈ V → suc 𝐴 = 𝐴)
76eqcomd 2742 . . . . 5 𝐴 ∈ V → 𝐴 = suc 𝐴)
8 ordeq 6324 . . . . 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 3445  Ord word 6316  suc csuc 6319
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
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 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-tr 5223  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-ord 6320  df-on 6321  df-suc 6323
This theorem is referenced by:  ordpwsuc  7749  onsucb  7751  ordsucss  7752  onpsssuc  7753  ordsucelsuc  7756  ordsucsssuc  7757  ordsucuniel  7758  ordsucun  7759  onsucuni2  7768  0elsuc  7769  nlimsucg  7777  limsssuc  7785  cofon1  8617  cofon2  8618  php4  9156  cantnflt  9607  fin23lem26  10260  hsmexlem1  10361  nosupres  27053  noetasuplem4  27082  noetainflem4  27086  scutbdaybnd2lim  27154  satfn  33940  onsuct0  34904  dfsucon  41777
  Copyright terms: Public domain W3C validator