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

Theorem suceloni 7517
Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
suceloni (𝐴 ∈ On → suc 𝐴 ∈ On)

Proof of Theorem suceloni
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 onelss 6226 . . . . . . . 8 (𝐴 ∈ On → (𝑥𝐴𝑥𝐴))
2 velsn 4573 . . . . . . . . . 10 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3 eqimss 4020 . . . . . . . . . 10 (𝑥 = 𝐴𝑥𝐴)
42, 3sylbi 218 . . . . . . . . 9 (𝑥 ∈ {𝐴} → 𝑥𝐴)
54a1i 11 . . . . . . . 8 (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥𝐴))
61, 5orim12d 958 . . . . . . 7 (𝐴 ∈ On → ((𝑥𝐴𝑥 ∈ {𝐴}) → (𝑥𝐴𝑥𝐴)))
7 df-suc 6190 . . . . . . . . 9 suc 𝐴 = (𝐴 ∪ {𝐴})
87eleq2i 2901 . . . . . . . 8 (𝑥 ∈ suc 𝐴𝑥 ∈ (𝐴 ∪ {𝐴}))
9 elun 4122 . . . . . . . 8 (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥𝐴𝑥 ∈ {𝐴}))
108, 9bitr2i 277 . . . . . . 7 ((𝑥𝐴𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴)
11 oridm 898 . . . . . . 7 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
126, 10, 113imtr3g 296 . . . . . 6 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥𝐴))
13 sssucid 6261 . . . . . 6 𝐴 ⊆ suc 𝐴
14 sstr2 3971 . . . . . 6 (𝑥𝐴 → (𝐴 ⊆ suc 𝐴𝑥 ⊆ suc 𝐴))
1512, 13, 14syl6mpi 67 . . . . 5 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴))
1615ralrimiv 3178 . . . 4 (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
17 dftr3 5167 . . . 4 (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
1816, 17sylibr 235 . . 3 (𝐴 ∈ On → Tr suc 𝐴)
19 onss 7494 . . . . 5 (𝐴 ∈ On → 𝐴 ⊆ On)
20 snssi 4733 . . . . 5 (𝐴 ∈ On → {𝐴} ⊆ On)
2119, 20unssd 4159 . . . 4 (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On)
227, 21eqsstrid 4012 . . 3 (𝐴 ∈ On → suc 𝐴 ⊆ On)
23 ordon 7487 . . . 4 Ord On
24 trssord 6201 . . . . 5 ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴)
25243exp 1111 . . . 4 (Tr suc 𝐴 → (suc 𝐴 ⊆ On → (Ord On → Ord suc 𝐴)))
2623, 25mpii 46 . . 3 (Tr suc 𝐴 → (suc 𝐴 ⊆ On → Ord suc 𝐴))
2718, 22, 26sylc 65 . 2 (𝐴 ∈ On → Ord suc 𝐴)
28 sucexg 7514 . . 3 (𝐴 ∈ On → suc 𝐴 ∈ V)
29 elong 6192 . . 3 (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
3028, 29syl 17 . 2 (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
3127, 30mpbird 258 1 (𝐴 ∈ On → suc 𝐴 ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wo 841   = wceq 1528  wcel 2105  wral 3135  Vcvv 3492  cun 3931  wss 3933  {csn 4557  Tr wtr 5163  Ord word 6183  Oncon0 6184  suc csuc 6186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-suc 6190
This theorem is referenced by:  ordsuc  7518  unon  7535  onsuci  7542  ordunisuc2  7548  ordzsl  7549  onzsl  7550  tfindsg  7564  dfom2  7571  findsg  7598  tfrlem12  8014  oasuc  8138  omsuc  8140  onasuc  8142  oacl  8149  oneo  8196  omeulem1  8197  omeulem2  8198  oeordi  8202  oeworde  8208  oelim2  8210  oelimcl  8215  oeeulem  8216  oeeui  8217  oaabs2  8261  omxpenlem  8606  card2inf  9007  cantnflt  9123  cantnflem1d  9139  cnfcom  9151  r1ordg  9195  bndrank  9258  r1pw  9262  r1pwALT  9263  tcrank  9301  onssnum  9454  dfac12lem2  9558  cfsuc  9667  cfsmolem  9680  fin1a2lem1  9810  fin1a2lem2  9811  ttukeylem7  9925  alephreg  9992  gch2  10085  winainflem  10103  winalim2  10106  r1wunlim  10147  nqereu  10339  noextend  33070  noresle  33097  nosupno  33100  ontgval  33676  ontgsucval  33677  onsuctop  33678  sucneqond  34528  onsetreclem2  44736
  Copyright terms: Public domain W3C validator