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

Theorem suceloni 7519
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 6230 . . . . . . . 8 (𝐴 ∈ On → (𝑥𝐴𝑥𝐴))
2 velsn 4579 . . . . . . . . . 10 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3 eqimss 4026 . . . . . . . . . 10 (𝑥 = 𝐴𝑥𝐴)
42, 3sylbi 218 . . . . . . . . 9 (𝑥 ∈ {𝐴} → 𝑥𝐴)
54a1i 11 . . . . . . . 8 (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥𝐴))
61, 5orim12d 960 . . . . . . 7 (𝐴 ∈ On → ((𝑥𝐴𝑥 ∈ {𝐴}) → (𝑥𝐴𝑥𝐴)))
7 df-suc 6194 . . . . . . . . 9 suc 𝐴 = (𝐴 ∪ {𝐴})
87eleq2i 2908 . . . . . . . 8 (𝑥 ∈ suc 𝐴𝑥 ∈ (𝐴 ∪ {𝐴}))
9 elun 4128 . . . . . . . 8 (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥𝐴𝑥 ∈ {𝐴}))
108, 9bitr2i 277 . . . . . . 7 ((𝑥𝐴𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴)
11 oridm 900 . . . . . . 7 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
126, 10, 113imtr3g 296 . . . . . 6 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥𝐴))
13 sssucid 6265 . . . . . 6 𝐴 ⊆ suc 𝐴
14 sstr2 3977 . . . . . 6 (𝑥𝐴 → (𝐴 ⊆ suc 𝐴𝑥 ⊆ suc 𝐴))
1512, 13, 14syl6mpi 67 . . . . 5 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴))
1615ralrimiv 3185 . . . 4 (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
17 dftr3 5172 . . . 4 (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
1816, 17sylibr 235 . . 3 (𝐴 ∈ On → Tr suc 𝐴)
19 onss 7496 . . . . 5 (𝐴 ∈ On → 𝐴 ⊆ On)
20 snssi 4739 . . . . 5 (𝐴 ∈ On → {𝐴} ⊆ On)
2119, 20unssd 4165 . . . 4 (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On)
227, 21eqsstrid 4018 . . 3 (𝐴 ∈ On → suc 𝐴 ⊆ On)
23 ordon 7489 . . . 4 Ord On
24 trssord 6205 . . . . 5 ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴)
25243exp 1113 . . . 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 7516 . . 3 (𝐴 ∈ On → suc 𝐴 ∈ V)
29 elong 6196 . . 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 843   = wceq 1530  wcel 2106  wral 3142  Vcvv 3499  cun 3937  wss 3939  {csn 4563  Tr wtr 5168  Ord word 6187  Oncon0 6188  suc csuc 6190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pr 5325  ax-un 7454
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-rab 3151  df-v 3501  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-br 5063  df-opab 5125  df-tr 5169  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-ord 6191  df-on 6192  df-suc 6194
This theorem is referenced by:  ordsuc  7520  unon  7537  onsuci  7544  ordunisuc2  7550  ordzsl  7551  onzsl  7552  tfindsg  7566  dfom2  7573  findsg  7600  tfrlem12  8019  oasuc  8143  omsuc  8145  onasuc  8147  oacl  8154  oneo  8200  omeulem1  8201  omeulem2  8202  oeordi  8206  oeworde  8212  oelim2  8214  oelimcl  8219  oeeulem  8220  oeeui  8221  oaabs2  8265  omxpenlem  8610  card2inf  9011  cantnflt  9127  cantnflem1d  9143  cnfcom  9155  r1ordg  9199  bndrank  9262  r1pw  9266  r1pwALT  9267  tcrank  9305  onssnum  9458  dfac12lem2  9562  cfsuc  9671  cfsmolem  9684  fin1a2lem1  9814  fin1a2lem2  9815  ttukeylem7  9929  alephreg  9996  gch2  10089  winainflem  10107  winalim2  10110  r1wunlim  10151  nqereu  10343  noextend  33058  noresle  33085  nosupno  33088  ontgval  33664  ontgsucval  33665  onsuctop  33666  sucneqond  34516  onsetreclem2  44637
  Copyright terms: Public domain W3C validator