Theorem limom 7815

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

Step	Hyp	Ref	Expression
1		ordom 7809	. 2 ⊢ Ord ω
2		ordeleqon 7718	. . 3 ⊢ (Ord ω ↔ (ω ∈ On ∨ ω = On))
3		ordirr 6325	. . . . . . 7 ⊢ (Ord ω → ¬ ω ∈ ω)
4	1, 3	ax-mp 5	. . . . . 6 ⊢ ¬ ω ∈ ω
5		elom 7802	. . . . . . 7 ⊢ (ω ∈ ω ↔ (ω ∈ On ∧ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
6	5	baib 535	. . . . . 6 ⊢ (ω ∈ On → (ω ∈ ω ↔ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
7	4, 6	mtbii 326	. . . . 5 ⊢ (ω ∈ On → ¬ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
8		limomss 7804	. . . . . . . . . . 11 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
9		limord 6368	. . . . . . . . . . . 12 ⊢ (Lim 𝑥 → Ord 𝑥)
10		ordsseleq 6336	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord 𝑥) → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
11	1, 9, 10	sylancr 587	. . . . . . . . . . 11 ⊢ (Lim 𝑥 → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
12	8, 11	mpbid 232	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (ω ∈ 𝑥 ∨ ω = 𝑥))
13	12	ord 864	. . . . . . . . 9 ⊢ (Lim 𝑥 → (¬ ω ∈ 𝑥 → ω = 𝑥))
14		limeq 6319	. . . . . . . . . 10 ⊢ (ω = 𝑥 → (Lim ω ↔ Lim 𝑥))
15	14	biimprcd 250	. . . . . . . . 9 ⊢ (Lim 𝑥 → (ω = 𝑥 → Lim ω))
16	13, 15	syld 47	. . . . . . . 8 ⊢ (Lim 𝑥 → (¬ ω ∈ 𝑥 → Lim ω))
17	16	con1d 145	. . . . . . 7 ⊢ (Lim 𝑥 → (¬ Lim ω → ω ∈ 𝑥))
18	17	com12 32	. . . . . 6 ⊢ (¬ Lim ω → (Lim 𝑥 → ω ∈ 𝑥))
19	18	alrimiv 1927	. . . . 5 ⊢ (¬ Lim ω → ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
20	7, 19	nsyl2 141	. . . 4 ⊢ (ω ∈ On → Lim ω)
21		limon 7769	. . . . 5 ⊢ Lim On
22		limeq 6319	. . . . 5 ⊢ (ω = On → (Lim ω ↔ Lim On))
23	21, 22	mpbiri 258	. . . 4 ⊢ (ω = On → Lim ω)
24	20, 23	jaoi 857	. . 3 ⊢ ((ω ∈ On ∨ ω = On) → Lim ω)
25	2, 24	sylbi 217	. 2 ⊢ (Ord ω → Lim ω)
26	1, 25	ax-mp 5	1 ⊢ Lim ω

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ⊆ wss 3903  Ord word 6306  Oncon0 6307  Lim wlim 6308  ωcom 7799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-tr 5200  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-om 7800

This theorem is referenced by:  peano2b  7816  ssnlim  7819  onesuc  8448  oaabslem  8565  oaabs2  8567  omabslem  8568  infensuc  9072  infeq5i  9532  elom3  9544  omenps  9551  omensuc  9552  infdifsn  9553  cardlim  9868  r1om  10137  cfom  10158  ominf4  10206  alephom  10479  wunex3  10635  satom  35333  fmla  35358  exrecfnlem  37357  onexlimgt  43220  oaabsb  43271  nnoeomeqom  43289  succlg  43305  dflim5  43306  dfom6  43508