Mathbox for Jim Kingdon |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > nconstwlpo | GIF version |
Description: Existence of a certain non-constant function from reals to integers implies ω ∈ WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.) |
Ref | Expression |
---|---|
nconstwlpo.f | ⊢ (𝜑 → 𝐹:ℝ⟶ℤ) |
nconstwlpo.0 | ⊢ (𝜑 → (𝐹‘0) = 0) |
nconstwlpo.rp | ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0) |
Ref | Expression |
---|---|
nconstwlpo | ⊢ (𝜑 → ω ∈ WOmni) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nconstwlpo.f | . . . . . . 7 ⊢ (𝜑 → 𝐹:ℝ⟶ℤ) | |
2 | 1 | adantr 274 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) → 𝐹:ℝ⟶ℤ) |
3 | nconstwlpo.0 | . . . . . . 7 ⊢ (𝜑 → (𝐹‘0) = 0) | |
4 | 3 | adantr 274 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) → (𝐹‘0) = 0) |
5 | nconstwlpo.rp | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0) | |
6 | 5 | adantlr 469 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) ∧ 𝑥 ∈ ℝ+) → (𝐹‘𝑥) ≠ 0) |
7 | elmapi 6608 | . . . . . . 7 ⊢ (𝑔 ∈ ({0, 1} ↑𝑚 ℕ) → 𝑔:ℕ⟶{0, 1}) | |
8 | 7 | adantl 275 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) → 𝑔:ℕ⟶{0, 1}) |
9 | oveq2 5826 | . . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (2↑𝑖) = (2↑𝑗)) | |
10 | 9 | oveq2d 5834 | . . . . . . . 8 ⊢ (𝑖 = 𝑗 → (1 / (2↑𝑖)) = (1 / (2↑𝑗))) |
11 | fveq2 5465 | . . . . . . . 8 ⊢ (𝑖 = 𝑗 → (𝑔‘𝑖) = (𝑔‘𝑗)) | |
12 | 10, 11 | oveq12d 5836 | . . . . . . 7 ⊢ (𝑖 = 𝑗 → ((1 / (2↑𝑖)) · (𝑔‘𝑖)) = ((1 / (2↑𝑗)) · (𝑔‘𝑗))) |
13 | 12 | cbvsumv 11240 | . . . . . 6 ⊢ Σ𝑖 ∈ ℕ ((1 / (2↑𝑖)) · (𝑔‘𝑖)) = Σ𝑗 ∈ ℕ ((1 / (2↑𝑗)) · (𝑔‘𝑗)) |
14 | 2, 4, 6, 8, 13 | nconstwlpolem 13598 | . . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) → (∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0)) |
15 | df-dc 821 | . . . . 5 ⊢ (DECID ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0 ↔ (∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0 ∨ ¬ ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0)) | |
16 | 14, 15 | sylibr 133 | . . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ ({0, 1} ↑𝑚 ℕ)) → DECID ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0) |
17 | 16 | ralrimiva 2530 | . . 3 ⊢ (𝜑 → ∀𝑔 ∈ ({0, 1} ↑𝑚 ℕ)DECID ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0) |
18 | nnex 8822 | . . . 4 ⊢ ℕ ∈ V | |
19 | iswomni0 13585 | . . . 4 ⊢ (ℕ ∈ V → (ℕ ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑𝑚 ℕ)DECID ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0)) | |
20 | 18, 19 | ax-mp 5 | . . 3 ⊢ (ℕ ∈ WOmni ↔ ∀𝑔 ∈ ({0, 1} ↑𝑚 ℕ)DECID ∀𝑦 ∈ ℕ (𝑔‘𝑦) = 0) |
21 | 17, 20 | sylibr 133 | . 2 ⊢ (𝜑 → ℕ ∈ WOmni) |
22 | nnenom 10315 | . . 3 ⊢ ℕ ≈ ω | |
23 | enwomni 7096 | . . 3 ⊢ (ℕ ≈ ω → (ℕ ∈ WOmni ↔ ω ∈ WOmni)) | |
24 | 22, 23 | ax-mp 5 | . 2 ⊢ (ℕ ∈ WOmni ↔ ω ∈ WOmni) |
25 | 21, 24 | sylib 121 | 1 ⊢ (𝜑 → ω ∈ WOmni) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 DECID wdc 820 = wceq 1335 ∈ wcel 2128 ≠ wne 2327 ∀wral 2435 Vcvv 2712 {cpr 3561 class class class wbr 3965 ωcom 4547 ⟶wf 5163 ‘cfv 5167 (class class class)co 5818 ↑𝑚 cmap 6586 ≈ cen 6676 WOmnicwomni 7089 ℝcr 7714 0cc0 7715 1c1 7716 · cmul 7720 / cdiv 8528 ℕcn 8816 2c2 8867 ℤcz 9150 ℝ+crp 9542 ↑cexp 10400 Σcsu 11232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4134 ax-pr 4168 ax-un 4392 ax-setind 4494 ax-iinf 4545 ax-cnex 7806 ax-resscn 7807 ax-1cn 7808 ax-1re 7809 ax-icn 7810 ax-addcl 7811 ax-addrcl 7812 ax-mulcl 7813 ax-mulrcl 7814 ax-addcom 7815 ax-mulcom 7816 ax-addass 7817 ax-mulass 7818 ax-distr 7819 ax-i2m1 7820 ax-0lt1 7821 ax-1rid 7822 ax-0id 7823 ax-rnegex 7824 ax-precex 7825 ax-cnre 7826 ax-pre-ltirr 7827 ax-pre-ltwlin 7828 ax-pre-lttrn 7829 ax-pre-apti 7830 ax-pre-ltadd 7831 ax-pre-mulgt0 7832 ax-pre-mulext 7833 ax-arch 7834 ax-caucvg 7835 |
This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-id 4252 df-po 4255 df-iso 4256 df-iord 4325 df-on 4327 df-ilim 4328 df-suc 4330 df-iom 4548 df-xp 4589 df-rel 4590 df-cnv 4591 df-co 4592 df-dm 4593 df-rn 4594 df-res 4595 df-ima 4596 df-iota 5132 df-fun 5169 df-fn 5170 df-f 5171 df-f1 5172 df-fo 5173 df-f1o 5174 df-fv 5175 df-isom 5176 df-riota 5774 df-ov 5821 df-oprab 5822 df-mpo 5823 df-1st 6082 df-2nd 6083 df-recs 6246 df-irdg 6311 df-frec 6332 df-1o 6357 df-2o 6358 df-oadd 6361 df-er 6473 df-map 6588 df-en 6679 df-dom 6680 df-fin 6681 df-womni 7090 df-pnf 7897 df-mnf 7898 df-xr 7899 df-ltxr 7900 df-le 7901 df-sub 8031 df-neg 8032 df-reap 8433 df-ap 8440 df-div 8529 df-inn 8817 df-2 8875 df-3 8876 df-4 8877 df-n0 9074 df-z 9151 df-uz 9423 df-q 9511 df-rp 9543 df-ico 9780 df-fz 9895 df-fzo 10024 df-seqfrec 10327 df-exp 10401 df-ihash 10632 df-cj 10724 df-re 10725 df-im 10726 df-rsqrt 10880 df-abs 10881 df-clim 11158 df-sumdc 11233 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |