Metamath Proof Explorer


Theorem opnmblALT

Description: All open sets are measurable. This alternative proof of opnmbl is significantly shorter, at the expense of invoking countable choice ax-cc . (This was also the original proof before the current opnmbl was discovered.) (Contributed by Mario Carneiro, 17-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion opnmblALT ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 qtopbas ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases
2 eltg3 ( ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases → ( 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∃ 𝑥 ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = 𝑥 ) ) )
3 1 2 ax-mp ( 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) ↔ ∃ 𝑥 ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = 𝑥 ) )
4 uniiun 𝑥 = 𝑦𝑥 𝑦
5 ssdomg ( ( (,) “ ( ℚ × ℚ ) ) ∈ TopBases → ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑥 ≼ ( (,) “ ( ℚ × ℚ ) ) ) )
6 1 5 ax-mp ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑥 ≼ ( (,) “ ( ℚ × ℚ ) ) )
7 omelon ω ∈ On
8 qnnen ℚ ≈ ℕ
9 xpen ( ( ℚ ≈ ℕ ∧ ℚ ≈ ℕ ) → ( ℚ × ℚ ) ≈ ( ℕ × ℕ ) )
10 8 8 9 mp2an ( ℚ × ℚ ) ≈ ( ℕ × ℕ )
11 xpnnen ( ℕ × ℕ ) ≈ ℕ
12 10 11 entri ( ℚ × ℚ ) ≈ ℕ
13 nnenom ℕ ≈ ω
14 12 13 entr2i ω ≈ ( ℚ × ℚ )
15 isnumi ( ( ω ∈ On ∧ ω ≈ ( ℚ × ℚ ) ) → ( ℚ × ℚ ) ∈ dom card )
16 7 14 15 mp2an ( ℚ × ℚ ) ∈ dom card
17 ioof (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
18 ffun ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
19 17 18 ax-mp Fun (,)
20 qssre ℚ ⊆ ℝ
21 ressxr ℝ ⊆ ℝ*
22 20 21 sstri ℚ ⊆ ℝ*
23 xpss12 ( ( ℚ ⊆ ℝ* ∧ ℚ ⊆ ℝ* ) → ( ℚ × ℚ ) ⊆ ( ℝ* × ℝ* ) )
24 22 22 23 mp2an ( ℚ × ℚ ) ⊆ ( ℝ* × ℝ* )
25 17 fdmi dom (,) = ( ℝ* × ℝ* )
26 24 25 sseqtrri ( ℚ × ℚ ) ⊆ dom (,)
27 fores ( ( Fun (,) ∧ ( ℚ × ℚ ) ⊆ dom (,) ) → ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) ) )
28 19 26 27 mp2an ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) )
29 fodomnum ( ( ℚ × ℚ ) ∈ dom card → ( ( (,) ↾ ( ℚ × ℚ ) ) : ( ℚ × ℚ ) –onto→ ( (,) “ ( ℚ × ℚ ) ) → ( (,) “ ( ℚ × ℚ ) ) ≼ ( ℚ × ℚ ) ) )
30 16 28 29 mp2 ( (,) “ ( ℚ × ℚ ) ) ≼ ( ℚ × ℚ )
31 domentr ( ( ( (,) “ ( ℚ × ℚ ) ) ≼ ( ℚ × ℚ ) ∧ ( ℚ × ℚ ) ≈ ℕ ) → ( (,) “ ( ℚ × ℚ ) ) ≼ ℕ )
32 30 12 31 mp2an ( (,) “ ( ℚ × ℚ ) ) ≼ ℕ
33 domtr ( ( 𝑥 ≼ ( (,) “ ( ℚ × ℚ ) ) ∧ ( (,) “ ( ℚ × ℚ ) ) ≼ ℕ ) → 𝑥 ≼ ℕ )
34 6 32 33 sylancl ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑥 ≼ ℕ )
35 imassrn ( (,) “ ( ℚ × ℚ ) ) ⊆ ran (,)
36 ffn ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
37 17 36 ax-mp (,) Fn ( ℝ* × ℝ* )
38 ioombl ( 𝑥 (,) 𝑦 ) ∈ dom vol
39 38 rgen2w 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ( 𝑥 (,) 𝑦 ) ∈ dom vol
40 ffnov ( (,) : ( ℝ* × ℝ* ) ⟶ dom vol ↔ ( (,) Fn ( ℝ* × ℝ* ) ∧ ∀ 𝑥 ∈ ℝ*𝑦 ∈ ℝ* ( 𝑥 (,) 𝑦 ) ∈ dom vol ) )
41 37 39 40 mpbir2an (,) : ( ℝ* × ℝ* ) ⟶ dom vol
42 frn ( (,) : ( ℝ* × ℝ* ) ⟶ dom vol → ran (,) ⊆ dom vol )
43 41 42 ax-mp ran (,) ⊆ dom vol
44 35 43 sstri ( (,) “ ( ℚ × ℚ ) ) ⊆ dom vol
45 sstr ( ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ ( (,) “ ( ℚ × ℚ ) ) ⊆ dom vol ) → 𝑥 ⊆ dom vol )
46 44 45 mpan2 ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑥 ⊆ dom vol )
47 dfss3 ( 𝑥 ⊆ dom vol ↔ ∀ 𝑦𝑥 𝑦 ∈ dom vol )
48 46 47 sylib ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → ∀ 𝑦𝑥 𝑦 ∈ dom vol )
49 iunmbl2 ( ( 𝑥 ≼ ℕ ∧ ∀ 𝑦𝑥 𝑦 ∈ dom vol ) → 𝑦𝑥 𝑦 ∈ dom vol )
50 34 48 49 syl2anc ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑦𝑥 𝑦 ∈ dom vol )
51 4 50 eqeltrid ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → 𝑥 ∈ dom vol )
52 eleq1 ( 𝐴 = 𝑥 → ( 𝐴 ∈ dom vol ↔ 𝑥 ∈ dom vol ) )
53 51 52 syl5ibrcom ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) → ( 𝐴 = 𝑥𝐴 ∈ dom vol ) )
54 53 imp ( ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = 𝑥 ) → 𝐴 ∈ dom vol )
55 54 exlimiv ( ∃ 𝑥 ( 𝑥 ⊆ ( (,) “ ( ℚ × ℚ ) ) ∧ 𝐴 = 𝑥 ) → 𝐴 ∈ dom vol )
56 3 55 sylbi ( 𝐴 ∈ ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) → 𝐴 ∈ dom vol )
57 eqid ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) ) = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
58 57 tgqioo ( topGen ‘ ran (,) ) = ( topGen ‘ ( (,) “ ( ℚ × ℚ ) ) )
59 56 58 eleq2s ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )