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

Theorem limom 7817
Description: Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. Theorem 1.23 of [Schloeder] p. 4. Our proof, however, does not require the Axiom of Infinity. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
limom Lim ω

Proof of Theorem limom
StepHypRef Expression
1 ordom 7811 . 2 Ord ω
2 ordeleqon 7715 . . 3 (Ord ω ↔ (ω ∈ On ∨ ω = On))
3 ordirr 6335 . . . . . . 7 (Ord ω → ¬ ω ∈ ω)
41, 3ax-mp 5 . . . . . 6 ¬ ω ∈ ω
5 elom 7804 . . . . . . 7 (ω ∈ ω ↔ (ω ∈ On ∧ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
65baib 536 . . . . . 6 (ω ∈ On → (ω ∈ ω ↔ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
74, 6mtbii 325 . . . . 5 (ω ∈ On → ¬ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
8 limomss 7806 . . . . . . . . . . 11 (Lim 𝑥 → ω ⊆ 𝑥)
9 limord 6377 . . . . . . . . . . . 12 (Lim 𝑥 → Ord 𝑥)
10 ordsseleq 6346 . . . . . . . . . . . 12 ((Ord ω ∧ Ord 𝑥) → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
111, 9, 10sylancr 587 . . . . . . . . . . 11 (Lim 𝑥 → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
128, 11mpbid 231 . . . . . . . . . 10 (Lim 𝑥 → (ω ∈ 𝑥 ∨ ω = 𝑥))
1312ord 862 . . . . . . . . 9 (Lim 𝑥 → (¬ ω ∈ 𝑥 → ω = 𝑥))
14 limeq 6329 . . . . . . . . . 10 (ω = 𝑥 → (Lim ω ↔ Lim 𝑥))
1514biimprcd 249 . . . . . . . . 9 (Lim 𝑥 → (ω = 𝑥 → Lim ω))
1613, 15syld 47 . . . . . . . 8 (Lim 𝑥 → (¬ ω ∈ 𝑥 → Lim ω))
1716con1d 145 . . . . . . 7 (Lim 𝑥 → (¬ Lim ω → ω ∈ 𝑥))
1817com12 32 . . . . . 6 (¬ Lim ω → (Lim 𝑥 → ω ∈ 𝑥))
1918alrimiv 1930 . . . . 5 (¬ Lim ω → ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
207, 19nsyl2 141 . . . 4 (ω ∈ On → Lim ω)
21 limon 7770 . . . . 5 Lim On
22 limeq 6329 . . . . 5 (ω = On → (Lim ω ↔ Lim On))
2321, 22mpbiri 257 . . . 4 (ω = On → Lim ω)
2420, 23jaoi 855 . . 3 ((ω ∈ On ∨ ω = On) → Lim ω)
252, 24sylbi 216 . 2 (Ord ω → Lim ω)
261, 25ax-mp 5 1 Lim ω
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wo 845  wal 1539   = wceq 1541  wcel 2106  wss 3910  Ord word 6316  Oncon0 6317  Lim wlim 6318  ωcom 7801
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  ax-un 7671
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-lim 6322  df-suc 6323  df-om 7802
This theorem is referenced by:  peano2b  7818  ssnlim  7821  peano1OLD  7825  onesuc  8475  oaabslem  8592  oaabs2  8594  omabslem  8595  infensuc  9098  infeq5i  9571  elom3  9583  omenps  9590  omensuc  9591  infdifsn  9592  cardlim  9907  r1om  10179  cfom  10199  ominf4  10247  alephom  10520  wunex3  10676  satom  33941  fmla  33966  exrecfnlem  35841  onexlimgt  41555  nnoeomeqom  41624  succlg  41640  dflim5  41641  dfom6  41785
  Copyright terms: Public domain W3C validator