opnvonmbllem2

Description: An open subset of the n-dimensional Real numbers is Lebesgue measurable. This is Proposition 115G (a) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	opnvonmbllem2.x	$⊢ φ \to X \in Fin$
	opnvonmbllem2.n	$⊢ S = dom voln (X)$
	opnvonmbllem2.g	$⊢ φ \to G \in TopOpen (X)$
	opnvonmbl.k	$⊢ K = \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
Assertion	opnvonmbllem2	$⊢ φ \to G \in S$

Proof

Step	Hyp	Ref	Expression
1		opnvonmbllem2.x	$⊢ φ \to X \in Fin$
2		opnvonmbllem2.n	$⊢ S = dom voln (X)$
3		opnvonmbllem2.g	$⊢ φ \to G \in TopOpen (X)$
4		opnvonmbl.k	$⊢ K = \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
5		eqid	$⊢ dist (X) = dist (X)$
6	5	rrxmetfi	$⊢ X \in Fin \to dist (X) \in Met (ℝ^{X})$
7	1 6	syl	$⊢ φ \to dist (X) \in Met (ℝ^{X})$
8		metxmet	$⊢ dist (X) \in Met (ℝ^{X}) \to dist (X) \in ∞Met (ℝ^{X})$
9	7 8	syl	$⊢ φ \to dist (X) \in ∞Met (ℝ^{X})$
10	9	adantr	$⊢ (φ \land x \in G) \to dist (X) \in ∞Met (ℝ^{X})$
11		eqid	$⊢ X = X$
12	11	rrxval	$⊢ X \in Fin \to X = toCPreHil (ℝ_{fld} freeLMod X)$
13	1 12	syl	$⊢ φ \to X = toCPreHil (ℝ_{fld} freeLMod X)$
14	13	fveq2d	$⊢ φ \to TopOpen (X) = TopOpen (toCPreHil (ℝ_{fld} freeLMod X))$
15		ovex	$⊢ ℝ_{fld} freeLMod X \in V$
16		eqid	$⊢ toCPreHil (ℝ_{fld} freeLMod X) = toCPreHil (ℝ_{fld} freeLMod X)$
17		eqid	$⊢ dist (toCPreHil (ℝ_{fld} freeLMod X)) = dist (toCPreHil (ℝ_{fld} freeLMod X))$
18		eqid	$⊢ TopOpen (toCPreHil (ℝ_{fld} freeLMod X)) = TopOpen (toCPreHil (ℝ_{fld} freeLMod X))$
19	16 17 18	tcphtopn	$⊢ ℝ_{fld} freeLMod X \in V \to TopOpen (toCPreHil (ℝ_{fld} freeLMod X)) = MetOpen (dist (toCPreHil (ℝ_{fld} freeLMod X)))$
20	15 19	ax-mp	$⊢ TopOpen (toCPreHil (ℝ_{fld} freeLMod X)) = MetOpen (dist (toCPreHil (ℝ_{fld} freeLMod X)))$
21	20	a1i	$⊢ φ \to TopOpen (toCPreHil (ℝ_{fld} freeLMod X)) = MetOpen (dist (toCPreHil (ℝ_{fld} freeLMod X)))$
22	13	eqcomd	$⊢ φ \to toCPreHil (ℝ_{fld} freeLMod X) = X$
23	22	fveq2d	$⊢ φ \to dist (toCPreHil (ℝ_{fld} freeLMod X)) = dist (X)$
24	23	fveq2d	$⊢ φ \to MetOpen (dist (toCPreHil (ℝ_{fld} freeLMod X))) = MetOpen (dist (X))$
25	14 21 24	3eqtrd	$⊢ φ \to TopOpen (X) = MetOpen (dist (X))$
26	3 25	eleqtrd	$⊢ φ \to G \in MetOpen (dist (X))$
27	26	adantr	$⊢ (φ \land x \in G) \to G \in MetOpen (dist (X))$
28		simpr	$⊢ (φ \land x \in G) \to x \in G$
29		eqid	$⊢ MetOpen (dist (X)) = MetOpen (dist (X))$
30	29	mopni2	$⊢ (dist (X) \in ∞Met (ℝ^{X}) \land G \in MetOpen (dist (X)) \land x \in G) \to \exists e \in ℝ^{+} x ball (dist (X)) e \subseteq G$
31	10 27 28 30	syl3anc	$⊢ (φ \land x \in G) \to \exists e \in ℝ^{+} x ball (dist (X)) e \subseteq G$
32	1	ad2antrr	$⊢ ((φ \land x \in G) \land e \in ℝ^{+}) \to X \in Fin$
33		eqid	$⊢ TopOpen (X) = TopOpen (X)$
34	33	rrxtoponfi	$⊢ X \in Fin \to TopOpen (X) \in TopOn (ℝ^{X})$
35	1 34	syl	$⊢ φ \to TopOpen (X) \in TopOn (ℝ^{X})$
36		toponss	$⊢ (TopOpen (X) \in TopOn (ℝ^{X}) \land G \in TopOpen (X)) \to G \subseteq ℝ^{X}$
37	35 3 36	syl2anc	$⊢ φ \to G \subseteq ℝ^{X}$
38	37	adantr	$⊢ (φ \land x \in G) \to G \subseteq ℝ^{X}$
39	38 28	sseldd	$⊢ (φ \land x \in G) \to x \in (ℝ^{X})$
40	39	adantr	$⊢ ((φ \land x \in G) \land e \in ℝ^{+}) \to x \in (ℝ^{X})$
41		simpr	$⊢ ((φ \land x \in G) \land e \in ℝ^{+}) \to e \in ℝ^{+}$
42	32 40 41	hoiqssbl	$⊢ ((φ \land x \in G) \land e \in ℝ^{+}) \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)$
43	42	3adant3	$⊢ ((φ \land x \in G) \land e \in ℝ^{+} \land x ball (dist (X)) e \subseteq G) \to \exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)$
44		nfv	$⊢ Ⅎ i (φ \land x ball (dist (X)) e \subseteq G)$
45		nfv	$⊢ Ⅎ i (c \in (ℚ^{X}) \land d \in (ℚ^{X}))$
46		nfcv	$⊢ \underline{Ⅎ} i x$
47		nfixp1	$⊢ \underline{Ⅎ} i \underset{i \in X}{⨉} [c (i), d (i))$
48	46 47	nfel	$⊢ Ⅎ i x \in \underset{i \in X}{⨉} [c (i), d (i))$
49		nfcv	$⊢ \underline{Ⅎ} i (x ball (dist (X)) e)$
50	47 49	nfss	$⊢ Ⅎ i \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e$
51	48 50	nfan	$⊢ Ⅎ i (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)$
52	44 45 51	nf3an	$⊢ Ⅎ i ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e))$
53	1	adantr	$⊢ (φ \land x ball (dist (X)) e \subseteq G) \to X \in Fin$
54	53	3ad2ant1	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to X \in Fin$
55		elmapi	$⊢ c \in (ℚ^{X}) \to c : X ⟶ ℚ$
56	55	adantr	$⊢ (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \to c : X ⟶ ℚ$
57	56	3ad2ant2	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to c : X ⟶ ℚ$
58		elmapi	$⊢ d \in (ℚ^{X}) \to d : X ⟶ ℚ$
59	58	adantl	$⊢ (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \to d : X ⟶ ℚ$
60	59	3ad2ant2	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to d : X ⟶ ℚ$
61		simp3r	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e$
62		simp1r	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to x ball (dist (X)) e \subseteq G$
63		simp3l	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to x \in \underset{i \in X}{⨉} [c (i), d (i))$
64		eqid	$⊢ (i \in X ⟼ ⟨c (i), d (i)⟩) = (i \in X ⟼ ⟨c (i), d (i)⟩)$
65	52 54 57 60 61 62 63 4 64	opnvonmbllem1	$⊢ ((φ \land x ball (dist (X)) e \subseteq G) \land (c \in (ℚ^{X}) \land d \in (ℚ^{X})) \land (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e)) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)$
66	65	3exp	$⊢ (φ \land x ball (dist (X)) e \subseteq G) \to ((c \in (ℚ^{X}) \land d \in (ℚ^{X})) \to ((x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)))$
67	66	adantlr	$⊢ ((φ \land x \in G) \land x ball (dist (X)) e \subseteq G) \to ((c \in (ℚ^{X}) \land d \in (ℚ^{X})) \to ((x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)))$
68	67	3adant2	$⊢ ((φ \land x \in G) \land e \in ℝ^{+} \land x ball (dist (X)) e \subseteq G) \to ((c \in (ℚ^{X}) \land d \in (ℚ^{X})) \to ((x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)))$
69	68	rexlimdvv	$⊢ ((φ \land x \in G) \land e \in ℝ^{+} \land x ball (dist (X)) e \subseteq G) \to (\exists c \in (ℚ^{X}) \exists d \in (ℚ^{X}) (x \in \underset{i \in X}{⨉} [c (i), d (i)) \land \underset{i \in X}{⨉} [c (i), d (i)) \subseteq x ball (dist (X)) e) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i))$
70	43 69	mpd	$⊢ ((φ \land x \in G) \land e \in ℝ^{+} \land x ball (dist (X)) e \subseteq G) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)$
71	70	3exp	$⊢ (φ \land x \in G) \to (e \in ℝ^{+} \to (x ball (dist (X)) e \subseteq G \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)))$
72	71	rexlimdv	$⊢ (φ \land x \in G) \to (\exists e \in ℝ^{+} x ball (dist (X)) e \subseteq G \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i))$
73	31 72	mpd	$⊢ (φ \land x \in G) \to \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)$
74		eliun	$⊢ x \in ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i) \leftrightarrow \exists h \in K x \in \underset{i \in X}{⨉} ([.) \circ h) (i)$
75	73 74	sylibr	$⊢ (φ \land x \in G) \to x \in ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i)$
76	75	ralrimiva	$⊢ φ \to \forall x \in G x \in ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i)$
77		dfss3	$⊢ G \subseteq ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i) \leftrightarrow \forall x \in G x \in ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i)$
78	76 77	sylibr	$⊢ φ \to G \subseteq ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i)$
79	4	eleq2i	$⊢ h \in K \leftrightarrow h \in \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
80	79	bilani	$⊢ (φ \land h \in K) \to h \in \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\}$
81		rabid	$⊢ h \in \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\} \leftrightarrow (h \in ({(ℚ \times ℚ)}^{X}) \land \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G)$
82	80 81	sylib	$⊢ (φ \land h \in K) \to (h \in ({(ℚ \times ℚ)}^{X}) \land \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G)$
83	82	simprd	$⊢ (φ \land h \in K) \to \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G$
84	83	ralrimiva	$⊢ φ \to \forall h \in K \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G$
85		iunss	$⊢ ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G \leftrightarrow \forall h \in K \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G$
86	84 85	sylibr	$⊢ φ \to ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G$
87	78 86	eqssd	$⊢ φ \to G = ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i)$
88	1 2	dmovnsal	$⊢ φ \to S \in SAlg$
89		ssrab2	$⊢ \{h \in ({(ℚ \times ℚ)}^{X}) \| \underset{i \in X}{⨉} ([.) \circ h) (i) \subseteq G\} \subseteq {(ℚ \times ℚ)}^{X}$
90	4 89	eqsstri	$⊢ K \subseteq {(ℚ \times ℚ)}^{X}$
91	90	a1i	$⊢ φ \to K \subseteq {(ℚ \times ℚ)}^{X}$
92		qct	$⊢ ℚ ≼ ω$
93	92	a1i	$⊢ φ \to ℚ ≼ ω$
94		xpct	$⊢ (ℚ ≼ ω \land ℚ ≼ ω) \to (ℚ \times ℚ) ≼ ω$
95	93 93 94	syl2anc	$⊢ φ \to (ℚ \times ℚ) ≼ ω$
96	95 1	mpct	$⊢ φ \to ({(ℚ \times ℚ)}^{X}) ≼ ω$
97		ssct	$⊢ (K \subseteq {(ℚ \times ℚ)}^{X} \land ({(ℚ \times ℚ)}^{X}) ≼ ω) \to K ≼ ω$
98	91 96 97	syl2anc	$⊢ φ \to K ≼ ω$
99		reex	$⊢ ℝ \in V$
100	99 99	xpex	$⊢ ℝ^{2} \in V$
101		qssre	$⊢ ℚ \subseteq ℝ$
102		xpss12	$⊢ (ℚ \subseteq ℝ \land ℚ \subseteq ℝ) \to ℚ \times ℚ \subseteq ℝ^{2}$
103	101 101 102	mp2an	$⊢ ℚ \times ℚ \subseteq ℝ^{2}$
104		mapss	$⊢ (ℝ^{2} \in V \land ℚ \times ℚ \subseteq ℝ^{2}) \to {(ℚ \times ℚ)}^{X} \subseteq {ℝ^{2}}^{X}$
105	100 103 104	mp2an	$⊢ {(ℚ \times ℚ)}^{X} \subseteq {ℝ^{2}}^{X}$
106	90	sseli	$⊢ h \in K \to h \in ({(ℚ \times ℚ)}^{X})$
107	105 106	sselid	$⊢ h \in K \to h \in ({ℝ^{2}}^{X})$
108		elmapi	$⊢ h \in ({ℝ^{2}}^{X}) \to h : X ⟶ ℝ^{2}$
109	107 108	syl	$⊢ h \in K \to h : X ⟶ ℝ^{2}$
110	109	adantl	$⊢ (φ \land h \in K) \to h : X ⟶ ℝ^{2}$
111		2fveq3	$⊢ k = i \to 1^{st} (h (k)) = 1^{st} (h (i))$
112	111	cbvmptv	$⊢ (k \in X ⟼ 1^{st} (h (k))) = (i \in X ⟼ 1^{st} (h (i)))$
113		2fveq3	$⊢ k = i \to 2^{nd} (h (k)) = 2^{nd} (h (i))$
114	113	cbvmptv	$⊢ (k \in X ⟼ 2^{nd} (h (k))) = (i \in X ⟼ 2^{nd} (h (i)))$
115	110 112 114	hoicoto2	$⊢ (φ \land h \in K) \to \underset{i \in X}{⨉} ([.) \circ h) (i) = \underset{i \in X}{⨉} [(k \in X ⟼ 1^{st} (h (k))) (i), (k \in X ⟼ 2^{nd} (h (k))) (i))$
116	1	adantr	$⊢ (φ \land h \in K) \to X \in Fin$
117	110	ffvelcdmda	$⊢ ((φ \land h \in K) \land k \in X) \to h (k) \in ℝ^{2}$
118		xp1st	$⊢ h (k) \in ℝ^{2} \to 1^{st} (h (k)) \in ℝ$
119	117 118	syl	$⊢ ((φ \land h \in K) \land k \in X) \to 1^{st} (h (k)) \in ℝ$
120	119	fmpttd	$⊢ (φ \land h \in K) \to (k \in X ⟼ 1^{st} (h (k))) : X ⟶ ℝ$
121		xp2nd	$⊢ h (k) \in ℝ^{2} \to 2^{nd} (h (k)) \in ℝ$
122	117 121	syl	$⊢ ((φ \land h \in K) \land k \in X) \to 2^{nd} (h (k)) \in ℝ$
123	122	fmpttd	$⊢ (φ \land h \in K) \to (k \in X ⟼ 2^{nd} (h (k))) : X ⟶ ℝ$
124	116 2 120 123	hoimbl	$⊢ (φ \land h \in K) \to \underset{i \in X}{⨉} [(k \in X ⟼ 1^{st} (h (k))) (i), (k \in X ⟼ 2^{nd} (h (k))) (i)) \in S$
125	115 124	eqeltrd	$⊢ (φ \land h \in K) \to \underset{i \in X}{⨉} ([.) \circ h) (i) \in S$
126	88 98 125	saliuncl	$⊢ φ \to ⋃_{h \in K} \underset{i \in X}{⨉} ([.) \circ h) (i) \in S$
127	87 126	eqeltrd	$⊢ φ \to G \in S$

Metamath Proof Explorer

Theorem opnvonmbllem2

Proof