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

Theorem suceloni 7511
 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 6202 . . . . . . . 8 (𝐴 ∈ On → (𝑥𝐴𝑥𝐴))
2 velsn 4541 . . . . . . . . . 10 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3 eqimss 3971 . . . . . . . . . 10 (𝑥 = 𝐴𝑥𝐴)
42, 3sylbi 220 . . . . . . . . 9 (𝑥 ∈ {𝐴} → 𝑥𝐴)
54a1i 11 . . . . . . . 8 (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥𝐴))
61, 5orim12d 962 . . . . . . 7 (𝐴 ∈ On → ((𝑥𝐴𝑥 ∈ {𝐴}) → (𝑥𝐴𝑥𝐴)))
7 df-suc 6166 . . . . . . . . 9 suc 𝐴 = (𝐴 ∪ {𝐴})
87eleq2i 2881 . . . . . . . 8 (𝑥 ∈ suc 𝐴𝑥 ∈ (𝐴 ∪ {𝐴}))
9 elun 4076 . . . . . . . 8 (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥𝐴𝑥 ∈ {𝐴}))
108, 9bitr2i 279 . . . . . . 7 ((𝑥𝐴𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴)
11 oridm 902 . . . . . . 7 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
126, 10, 113imtr3g 298 . . . . . 6 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥𝐴))
13 sssucid 6237 . . . . . 6 𝐴 ⊆ suc 𝐴
14 sstr2 3922 . . . . . 6 (𝑥𝐴 → (𝐴 ⊆ suc 𝐴𝑥 ⊆ suc 𝐴))
1512, 13, 14syl6mpi 67 . . . . 5 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴))
1615ralrimiv 3148 . . . 4 (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
17 dftr3 5141 . . . 4 (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
1816, 17sylibr 237 . . 3 (𝐴 ∈ On → Tr suc 𝐴)
19 onss 7488 . . . . 5 (𝐴 ∈ On → 𝐴 ⊆ On)
20 snssi 4701 . . . . 5 (𝐴 ∈ On → {𝐴} ⊆ On)
2119, 20unssd 4113 . . . 4 (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On)
227, 21eqsstrid 3963 . . 3 (𝐴 ∈ On → suc 𝐴 ⊆ On)
23 ordon 7481 . . . 4 Ord On
24 trssord 6177 . . . . 5 ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴)
25243exp 1116 . . . 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 7508 . . 3 (𝐴 ∈ On → suc 𝐴 ∈ V)
29 elong 6168 . . 3 (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
3028, 29syl 17 . 2 (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴))
3127, 30mpbird 260 1 (𝐴 ∈ On → suc 𝐴 ∈ On)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  {csn 4525  Tr wtr 5137  Ord word 6159  Oncon0 6160  suc csuc 6162 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-br 5032  df-opab 5094  df-tr 5138  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-ord 6163  df-on 6164  df-suc 6166 This theorem is referenced by:  ordsuc  7512  unon  7529  onsuci  7536  ordunisuc2  7542  ordzsl  7543  onzsl  7544  tfindsg  7558  dfom2  7565  findsg  7593  tfrlem12  8011  oasuc  8135  omsuc  8137  onasuc  8139  oacl  8146  oneo  8193  omeulem1  8194  omeulem2  8195  oeordi  8199  oeworde  8205  oelim2  8207  oelimcl  8212  oeeulem  8213  oeeui  8214  oaabs2  8258  omxpenlem  8604  card2inf  9006  cantnflt  9122  cantnflem1d  9138  cnfcom  9150  r1ordg  9194  bndrank  9257  r1pw  9261  r1pwALT  9262  tcrank  9300  onssnum  9454  dfac12lem2  9558  cfsuc  9671  cfsmolem  9684  fin1a2lem1  9814  fin1a2lem2  9815  ttukeylem7  9929  alephreg  9996  gch2  10089  winainflem  10107  winalim2  10110  r1wunlim  10151  nqereu  10343  noextend  33301  noresle  33328  nosupno  33331  ontgval  33907  ontgsucval  33908  onsuctop  33909  sucneqond  34801  onsetreclem2  45276
 Copyright terms: Public domain W3C validator