| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > opnmbl | Structured version Visualization version GIF version | ||
| Description: All open sets are measurable. This proof, via dyadmbl 25572 and uniioombl 25561, shows that it is possible to avoid choice for measurability of open sets and hence continuous functions, which extends the choice-free consequences of Lebesgue measure considerably farther than would otherwise be possible. (Contributed by Mario Carneiro, 26-Mar-2015.) |
| Ref | Expression |
|---|---|
| opnmbl | ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oveq1 7420 | . . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 / (2↑𝑦)) = (𝑧 / (2↑𝑦))) | |
| 2 | oveq1 7420 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 + 1) = (𝑧 + 1)) | |
| 3 | 2 | oveq1d 7428 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑧 + 1) / (2↑𝑦))) |
| 4 | 1, 3 | opeq12d 4861 | . . 3 ⊢ (𝑥 = 𝑧 → 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉 = 〈(𝑧 / (2↑𝑦)), ((𝑧 + 1) / (2↑𝑦))〉) |
| 5 | oveq2 7421 | . . . . 5 ⊢ (𝑦 = 𝑤 → (2↑𝑦) = (2↑𝑤)) | |
| 6 | 5 | oveq2d 7429 | . . . 4 ⊢ (𝑦 = 𝑤 → (𝑧 / (2↑𝑦)) = (𝑧 / (2↑𝑤))) |
| 7 | 5 | oveq2d 7429 | . . . 4 ⊢ (𝑦 = 𝑤 → ((𝑧 + 1) / (2↑𝑦)) = ((𝑧 + 1) / (2↑𝑤))) |
| 8 | 6, 7 | opeq12d 4861 | . . 3 ⊢ (𝑦 = 𝑤 → 〈(𝑧 / (2↑𝑦)), ((𝑧 + 1) / (2↑𝑦))〉 = 〈(𝑧 / (2↑𝑤)), ((𝑧 + 1) / (2↑𝑤))〉) |
| 9 | 4, 8 | cbvmpov 7510 | . 2 ⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) = (𝑧 ∈ ℤ, 𝑤 ∈ ℕ0 ↦ 〈(𝑧 / (2↑𝑤)), ((𝑧 + 1) / (2↑𝑤))〉) |
| 10 | 9 | opnmbllem 25573 | 1 ⊢ (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2107 〈cop 4612 dom cdm 5665 ran crn 5666 ‘cfv 6541 (class class class)co 7413 ∈ cmpo 7415 1c1 11138 + caddc 11140 / cdiv 11902 2c2 12303 ℕ0cn0 12509 ℤcz 12596 (,)cioo 13369 ↑cexp 14084 topGenctg 17454 volcvol 25435 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-inf2 9663 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-disj 5091 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-om 7870 df-1st 7996 df-2nd 7997 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-omul 8493 df-er 8727 df-map 8850 df-pm 8851 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9532 df-dju 9923 df-card 9961 df-acn 9964 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-n0 12510 df-z 12597 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13373 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13677 df-fl 13814 df-seq 14025 df-exp 14085 df-hash 14353 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-clim 15507 df-rlim 15508 df-sum 15706 df-rest 17439 df-topgen 17460 df-psmet 21319 df-xmet 21320 df-met 21321 df-bl 21322 df-mopn 21323 df-top 22849 df-topon 22866 df-bases 22901 df-cmp 23342 df-ovol 25436 df-vol 25437 |
| This theorem is referenced by: subopnmbl 25576 mblfinlem3 37641 mblfinlem4 37642 ismblfin 37643 |
| Copyright terms: Public domain | W3C validator |