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 )

Metamath Proof Explorer

Theorem opnmblALT

Proof