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

Theorem suceloni 7592
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 6255 . . . . . . . 8 (𝐴 ∈ On → (𝑥𝐴𝑥𝐴))
2 velsn 4557 . . . . . . . . . 10 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
3 eqimss 3957 . . . . . . . . . 10 (𝑥 = 𝐴𝑥𝐴)
42, 3sylbi 220 . . . . . . . . 9 (𝑥 ∈ {𝐴} → 𝑥𝐴)
54a1i 11 . . . . . . . 8 (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥𝐴))
61, 5orim12d 965 . . . . . . 7 (𝐴 ∈ On → ((𝑥𝐴𝑥 ∈ {𝐴}) → (𝑥𝐴𝑥𝐴)))
7 df-suc 6219 . . . . . . . . 9 suc 𝐴 = (𝐴 ∪ {𝐴})
87eleq2i 2829 . . . . . . . 8 (𝑥 ∈ suc 𝐴𝑥 ∈ (𝐴 ∪ {𝐴}))
9 elun 4063 . . . . . . . 8 (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥𝐴𝑥 ∈ {𝐴}))
108, 9bitr2i 279 . . . . . . 7 ((𝑥𝐴𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴)
11 oridm 905 . . . . . . 7 ((𝑥𝐴𝑥𝐴) ↔ 𝑥𝐴)
126, 10, 113imtr3g 298 . . . . . 6 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥𝐴))
13 sssucid 6290 . . . . . 6 𝐴 ⊆ suc 𝐴
14 sstr2 3908 . . . . . 6 (𝑥𝐴 → (𝐴 ⊆ suc 𝐴𝑥 ⊆ suc 𝐴))
1512, 13, 14syl6mpi 67 . . . . 5 (𝐴 ∈ On → (𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴))
1615ralrimiv 3104 . . . 4 (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
17 dftr3 5165 . . . 4 (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴)
1816, 17sylibr 237 . . 3 (𝐴 ∈ On → Tr suc 𝐴)
19 onss 7568 . . . . 5 (𝐴 ∈ On → 𝐴 ⊆ On)
20 snssi 4721 . . . . 5 (𝐴 ∈ On → {𝐴} ⊆ On)
2119, 20unssd 4100 . . . 4 (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On)
227, 21eqsstrid 3949 . . 3 (𝐴 ∈ On → suc 𝐴 ⊆ On)
23 ordon 7561 . . . 4 Ord On
24 trssord 6230 . . . . 5 ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴)
25243exp 1121 . . . 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 7589 . . 3 (𝐴 ∈ On → suc 𝐴 ∈ V)
29 elong 6221 . . 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 847   = wceq 1543  wcel 2110  wral 3061  Vcvv 3408  cun 3864  wss 3866  {csn 4541  Tr wtr 5161  Ord word 6212  Oncon0 6213  suc csuc 6215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-tr 5162  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-ord 6216  df-on 6217  df-suc 6219
This theorem is referenced by:  ordsuc  7593  unon  7610  onsuci  7617  ordunisuc2  7623  ordzsl  7624  onzsl  7625  tfindsg  7639  dfom2  7646  findsg  7677  tfrlem12  8125  oasuc  8251  omsuc  8253  onasuc  8255  oacl  8262  oneo  8309  omeulem1  8310  omeulem2  8311  oeordi  8315  oeworde  8321  oelim2  8323  oelimcl  8328  oeeulem  8329  oeeui  8330  oaabs2  8374  omxpenlem  8746  card2inf  9171  cantnflt  9287  cantnflem1d  9303  cnfcom  9315  r1ordg  9394  bndrank  9457  r1pw  9461  r1pwALT  9462  tcrank  9500  onssnum  9654  dfac12lem2  9758  cfsuc  9871  cfsmolem  9884  fin1a2lem1  10014  fin1a2lem2  10015  ttukeylem7  10129  alephreg  10196  gch2  10289  winainflem  10307  winalim2  10310  r1wunlim  10351  nqereu  10543  noextend  33606  noresle  33637  nosupno  33643  madeoldsuc  33804  ontgval  34357  ontgsucval  34358  onsuctop  34359  sucneqond  35273  onsetreclem2  46082
  Copyright terms: Public domain W3C validator