![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limom | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
limom | ⊢ Lim ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordom 7811 | . 2 ⊢ Ord ω | |
2 | ordeleqon 7715 | . . 3 ⊢ (Ord ω ↔ (ω ∈ On ∨ ω = On)) | |
3 | ordirr 6335 | . . . . . . 7 ⊢ (Ord ω → ¬ ω ∈ ω) | |
4 | 1, 3 | ax-mp 5 | . . . . . 6 ⊢ ¬ ω ∈ ω |
5 | elom 7804 | . . . . . . 7 ⊢ (ω ∈ ω ↔ (ω ∈ On ∧ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))) | |
6 | 5 | baib 536 | . . . . . 6 ⊢ (ω ∈ On → (ω ∈ ω ↔ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥))) |
7 | 4, 6 | mtbii 325 | . . . . 5 ⊢ (ω ∈ On → ¬ ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)) |
8 | limomss 7806 | . . . . . . . . . . 11 ⊢ (Lim 𝑥 → ω ⊆ 𝑥) | |
9 | limord 6377 | . . . . . . . . . . . 12 ⊢ (Lim 𝑥 → Ord 𝑥) | |
10 | ordsseleq 6346 | . . . . . . . . . . . 12 ⊢ ((Ord ω ∧ Ord 𝑥) → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥))) | |
11 | 1, 9, 10 | sylancr 587 | . . . . . . . . . . 11 ⊢ (Lim 𝑥 → (ω ⊆ 𝑥 ↔ (ω ∈ 𝑥 ∨ ω = 𝑥))) |
12 | 8, 11 | mpbid 231 | . . . . . . . . . 10 ⊢ (Lim 𝑥 → (ω ∈ 𝑥 ∨ ω = 𝑥)) |
13 | 12 | ord 862 | . . . . . . . . 9 ⊢ (Lim 𝑥 → (¬ ω ∈ 𝑥 → ω = 𝑥)) |
14 | limeq 6329 | . . . . . . . . . 10 ⊢ (ω = 𝑥 → (Lim ω ↔ Lim 𝑥)) | |
15 | 14 | biimprcd 249 | . . . . . . . . 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 1930 | . . . . 5 ⊢ (¬ Lim ω → ∀𝑥(Lim 𝑥 → ω ∈ 𝑥)) |
20 | 7, 19 | nsyl2 141 | . . . 4 ⊢ (ω ∈ On → Lim ω) |
21 | limon 7770 | . . . . 5 ⊢ Lim On | |
22 | limeq 6329 | . . . . 5 ⊢ (ω = On → (Lim ω ↔ Lim On)) | |
23 | 21, 22 | mpbiri 257 | . . . 4 ⊢ (ω = On → Lim ω) |
24 | 20, 23 | jaoi 855 | . . 3 ⊢ ((ω ∈ On ∨ ω = On) → Lim ω) |
25 | 2, 24 | sylbi 216 | . 2 ⊢ (Ord ω → Lim ω) |
26 | 1, 25 | ax-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 |