Theorem limom 7884

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 7878	. 2 ⊢ Ord ω
2		ordeleqon 7787	. . 3 ⊢ (Ord ω ↔ (ω ∈ On ∨ ω = On))
3		ordirr 6382	. . . . . . 7 ⊢ (Ord ω → ¬ ω ∈ ω)
4	1, 3	ax-mp 5	. . . . . 6 ⊢ ¬ ω ∈ ω
5		elom 7871	. . . . . . 7 ⊢ (ω ∈ ω ↔ (ω ∈ On ∧ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
6	5	baib 545	. . . . . 6 ⊢ (ω ∈ On → (ω ∈ ω ↔ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)))
7	4, 6	mtbii 329	. . . . 5 ⊢ (ω ∈ On → ¬ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
8		limomss 7873	. . . . . . . . . . 11 ⊢ (Lim 𝑥 → ω ⊆ 𝑥)
9		limord 6426	. . . . . . . . . . . 12 ⊢ (Lim 𝑥 → Ord 𝑥)
10		ordsseleq 6394	. . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord 𝑥) → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
11	1, 9, 10	sylancr 599	. . . . . . . . . . 11 ⊢ (Lim 𝑥 → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥)))
12	8, 11	mpbid 235	. . . . . . . . . 10 ⊢ (Lim 𝑥 → (ω ∈ 𝑥 ∨ ω = 𝑥))
13	12	ord 878	. . . . . . . . 9 ⊢ (Lim 𝑥 → (¬ ω ∈ 𝑥 → ω = 𝑥))
14		limeq 6376	. . . . . . . . . 10 ⊢ (ω = 𝑥 → (Lim ω ↔ Lim 𝑥))
15	14	biimprcd 253	. . . . . . . . 9 ⊢ (Lim 𝑥 → (ω = 𝑥 → Lim ω))
16	13, 15	syld 48	. . . . . . . 8 ⊢ (Lim 𝑥 → (¬ ω ∈ 𝑥 → Lim ω))
17	16	con1d 146	. . . . . . 7 ⊢ (Lim 𝑥 → (¬ Lim ω → ω ∈ 𝑥))
18	17	com12 33	. . . . . 6 ⊢ (¬ Lim ω → (Lim 𝑥 → ω ∈ 𝑥))
19	18	alrimiv 1960	. . . . 5 ⊢ (¬ Lim ω → ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))
20	7, 19	nsyl2 142	. . . 4 ⊢ (ω ∈ On → Lim ω)
21		limon 7838	. . . . 5 ⊢ Lim On
22		limeq 6376	. . . . 5 ⊢ (ω = On → (Lim ω ↔ Lim On))
23	21, 22	mpbiri 261	. . . 4 ⊢ (ω = On → Lim ω)
24	20, 23	jaoi 871	. . 3 ⊢ ((ω ∈ On ∨ ω = On) → Lim ω)
25	2, 24	sylbi 220	. 2 ⊢ (Ord ω → Lim ω)
26	1, 25	ax-mp 5	1 ⊢ Lim ω

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2146   ⊆ wss 3906  Ord word 6363  Oncon0 6364  Lim wlim 6365  ωcom 7868

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-tr 5221  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-om 7869

This theorem is used by:  peano2b  7885  ssnlim  7888  onesuc  8521  oaabslem  8639  oaabs2  8641  omabslem  8642  infensuc  9150  infeq5i  9612  elom3  9624  omenps  9631  omensuc  9632  infdifsn  9633  cardlim  9974  r1om  10242  cfom  10263  ominf4  10311  alephom  10587  wunex3  10743  r1omhf  35560  r1omfv  35564  satom  35887  fmla  35912  exrecfnlem  38084  onexlimgt  44030  oaabsb  44081  nnoeomeqom  44099  succlg  44115  dflim5  44116  dfom6  44317