MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opnmblALT Structured version   Visualization version   GIF version

Theorem opnmblALT 23660
Description: All open sets are measurable. This alternative proof of opnmbl 23659 is significantly shorter, at the expense of invoking countable choice ax-cc 9509. (This was also the original proof before the current opnmbl 23659 was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
opnmblALT (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)

Proof of Theorem opnmblALT
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 qtopbas 22841 . . . 4 ((,) “ (ℚ × ℚ)) ∈ TopBases
2 eltg3 21045 . . . 4 (((,) “ (ℚ × ℚ)) ∈ TopBases → (𝐴 ∈ (topGen‘((,) “ (ℚ × ℚ))) ↔ ∃𝑥(𝑥 ⊆ ((,) “ (ℚ × ℚ)) ∧ 𝐴 = 𝑥)))
31, 2ax-mp 5 . . 3 (𝐴 ∈ (topGen‘((,) “ (ℚ × ℚ))) ↔ ∃𝑥(𝑥 ⊆ ((,) “ (ℚ × ℚ)) ∧ 𝐴 = 𝑥))
4 uniiun 4728 . . . . . . 7 𝑥 = 𝑦𝑥 𝑦
5 ssdomg 8205 . . . . . . . . . 10 (((,) “ (ℚ × ℚ)) ∈ TopBases → (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑥 ≼ ((,) “ (ℚ × ℚ))))
61, 5ax-mp 5 . . . . . . . . 9 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑥 ≼ ((,) “ (ℚ × ℚ)))
7 omelon 8757 . . . . . . . . . . . 12 ω ∈ On
8 qnnen 15225 . . . . . . . . . . . . . . 15 ℚ ≈ ℕ
9 xpen 8329 . . . . . . . . . . . . . . 15 ((ℚ ≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ) ≈ (ℕ × ℕ))
108, 8, 9mp2an 683 . . . . . . . . . . . . . 14 (ℚ × ℚ) ≈ (ℕ × ℕ)
11 xpnnen 15222 . . . . . . . . . . . . . 14 (ℕ × ℕ) ≈ ℕ
1210, 11entri 8213 . . . . . . . . . . . . 13 (ℚ × ℚ) ≈ ℕ
13 nnenom 12986 . . . . . . . . . . . . 13 ℕ ≈ ω
1412, 13entr2i 8214 . . . . . . . . . . . 12 ω ≈ (ℚ × ℚ)
15 isnumi 9022 . . . . . . . . . . . 12 ((ω ∈ On ∧ ω ≈ (ℚ × ℚ)) → (ℚ × ℚ) ∈ dom card)
167, 14, 15mp2an 683 . . . . . . . . . . 11 (ℚ × ℚ) ∈ dom card
17 ioof 12473 . . . . . . . . . . . . 13 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
18 ffun 6225 . . . . . . . . . . . . 13 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
1917, 18ax-mp 5 . . . . . . . . . . . 12 Fun (,)
20 qssre 11998 . . . . . . . . . . . . . . 15 ℚ ⊆ ℝ
21 ressxr 10336 . . . . . . . . . . . . . . 15 ℝ ⊆ ℝ*
2220, 21sstri 3769 . . . . . . . . . . . . . 14 ℚ ⊆ ℝ*
23 xpss12 5291 . . . . . . . . . . . . . 14 ((ℚ ⊆ ℝ* ∧ ℚ ⊆ ℝ*) → (ℚ × ℚ) ⊆ (ℝ* × ℝ*))
2422, 22, 23mp2an 683 . . . . . . . . . . . . 13 (ℚ × ℚ) ⊆ (ℝ* × ℝ*)
2517fdmi 6232 . . . . . . . . . . . . 13 dom (,) = (ℝ* × ℝ*)
2624, 25sseqtr4i 3797 . . . . . . . . . . . 12 (ℚ × ℚ) ⊆ dom (,)
27 fores 6306 . . . . . . . . . . . 12 ((Fun (,) ∧ (ℚ × ℚ) ⊆ dom (,)) → ((,) ↾ (ℚ × ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ × ℚ)))
2819, 26, 27mp2an 683 . . . . . . . . . . 11 ((,) ↾ (ℚ × ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ × ℚ))
29 fodomnum 9130 . . . . . . . . . . 11 ((ℚ × ℚ) ∈ dom card → (((,) ↾ (ℚ × ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ × ℚ)) → ((,) “ (ℚ × ℚ)) ≼ (ℚ × ℚ)))
3016, 28, 29mp2 9 . . . . . . . . . 10 ((,) “ (ℚ × ℚ)) ≼ (ℚ × ℚ)
31 domentr 8218 . . . . . . . . . 10 ((((,) “ (ℚ × ℚ)) ≼ (ℚ × ℚ) ∧ (ℚ × ℚ) ≈ ℕ) → ((,) “ (ℚ × ℚ)) ≼ ℕ)
3230, 12, 31mp2an 683 . . . . . . . . 9 ((,) “ (ℚ × ℚ)) ≼ ℕ
33 domtr 8212 . . . . . . . . 9 ((𝑥 ≼ ((,) “ (ℚ × ℚ)) ∧ ((,) “ (ℚ × ℚ)) ≼ ℕ) → 𝑥 ≼ ℕ)
346, 32, 33sylancl 580 . . . . . . . 8 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑥 ≼ ℕ)
35 imassrn 5658 . . . . . . . . . . 11 ((,) “ (ℚ × ℚ)) ⊆ ran (,)
36 ffn 6222 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
3717, 36ax-mp 5 . . . . . . . . . . . . 13 (,) Fn (ℝ* × ℝ*)
38 ioombl 23622 . . . . . . . . . . . . . 14 (𝑥(,)𝑦) ∈ dom vol
3938rgen2w 3071 . . . . . . . . . . . . 13 𝑥 ∈ ℝ*𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ dom vol
40 ffnov 6961 . . . . . . . . . . . . 13 ((,):(ℝ* × ℝ*)⟶dom vol ↔ ((,) Fn (ℝ* × ℝ*) ∧ ∀𝑥 ∈ ℝ*𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ dom vol))
4137, 39, 40mpbir2an 702 . . . . . . . . . . . 12 (,):(ℝ* × ℝ*)⟶dom vol
42 frn 6228 . . . . . . . . . . . 12 ((,):(ℝ* × ℝ*)⟶dom vol → ran (,) ⊆ dom vol)
4341, 42ax-mp 5 . . . . . . . . . . 11 ran (,) ⊆ dom vol
4435, 43sstri 3769 . . . . . . . . . 10 ((,) “ (ℚ × ℚ)) ⊆ dom vol
45 sstr 3768 . . . . . . . . . 10 ((𝑥 ⊆ ((,) “ (ℚ × ℚ)) ∧ ((,) “ (ℚ × ℚ)) ⊆ dom vol) → 𝑥 ⊆ dom vol)
4644, 45mpan2 682 . . . . . . . . 9 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑥 ⊆ dom vol)
47 dfss3 3749 . . . . . . . . 9 (𝑥 ⊆ dom vol ↔ ∀𝑦𝑥 𝑦 ∈ dom vol)
4846, 47sylib 209 . . . . . . . 8 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → ∀𝑦𝑥 𝑦 ∈ dom vol)
49 iunmbl2 23614 . . . . . . . 8 ((𝑥 ≼ ℕ ∧ ∀𝑦𝑥 𝑦 ∈ dom vol) → 𝑦𝑥 𝑦 ∈ dom vol)
5034, 48, 49syl2anc 579 . . . . . . 7 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑦𝑥 𝑦 ∈ dom vol)
514, 50syl5eqel 2847 . . . . . 6 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → 𝑥 ∈ dom vol)
52 eleq1 2831 . . . . . 6 (𝐴 = 𝑥 → (𝐴 ∈ dom vol ↔ 𝑥 ∈ dom vol))
5351, 52syl5ibrcom 238 . . . . 5 (𝑥 ⊆ ((,) “ (ℚ × ℚ)) → (𝐴 = 𝑥𝐴 ∈ dom vol))
5453imp 395 . . . 4 ((𝑥 ⊆ ((,) “ (ℚ × ℚ)) ∧ 𝐴 = 𝑥) → 𝐴 ∈ dom vol)
5554exlimiv 2025 . . 3 (∃𝑥(𝑥 ⊆ ((,) “ (ℚ × ℚ)) ∧ 𝐴 = 𝑥) → 𝐴 ∈ dom vol)
563, 55sylbi 208 . 2 (𝐴 ∈ (topGen‘((,) “ (ℚ × ℚ))) → 𝐴 ∈ dom vol)
57 eqid 2764 . . 3 (topGen‘((,) “ (ℚ × ℚ))) = (topGen‘((,) “ (ℚ × ℚ)))
5857tgqioo 22881 . 2 (topGen‘ran (,)) = (topGen‘((,) “ (ℚ × ℚ)))
5956, 58eleq2s 2861 1 (𝐴 ∈ (topGen‘ran (,)) → 𝐴 ∈ dom vol)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wex 1874  wcel 2155  wral 3054  wss 3731  𝒫 cpw 4314   cuni 4593   ciun 4675   class class class wbr 4808   × cxp 5274  dom cdm 5276  ran crn 5277  cres 5278  cima 5279  Oncon0 5907  Fun wfun 6061   Fn wfn 6062  wf 6063  ontowfo 6065  cfv 6067  (class class class)co 6841  ωcom 7262  cen 8156  cdom 8157  cardccrd 9011  cr 10187  *cxr 10326  cn 11273  cq 11988  (,)cioo 12376  topGenctg 16365  TopBasesctb 21028  volcvol 23520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-inf2 8752  ax-cc 9509  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-pre-sup 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-disj 4777  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-of 7094  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-2o 7764  df-oadd 7767  df-omul 7768  df-er 7946  df-map 8061  df-pm 8062  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-sup 8554  df-inf 8555  df-oi 8621  df-card 9015  df-acn 9018  df-cda 9242  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-div 10938  df-nn 11274  df-2 11334  df-3 11335  df-n0 11538  df-z 11624  df-uz 11886  df-q 11989  df-rp 12028  df-xadd 12146  df-ioo 12380  df-ico 12382  df-icc 12383  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14125  df-re 14126  df-im 14127  df-sqrt 14261  df-abs 14262  df-clim 14505  df-rlim 14506  df-sum 14703  df-topgen 16371  df-xmet 20011  df-met 20012  df-bases 21029  df-ovol 23521  df-vol 23522
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator