opnvonmbllem2 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > opnvonmbllem2		Structured version Visualization version GIF version

Theorem opnvonmbllem2 44560

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.)

**Hypotheses**
Ref	Expression
opnvonmbllem2.x	⊢ (𝜑 → 𝑋 ∈ Fin)
opnvonmbllem2.n	⊢ 𝑆 = dom (voln‘𝑋)
opnvonmbllem2.g	⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
opnvonmbl.k	⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}

**Assertion**
Ref	Expression
opnvonmbllem2	⊢ (𝜑 → 𝐺 ∈ 𝑆)

Distinct variable groups: ℎ,𝐺,𝑖 ℎ,𝐾,𝑖 𝑆,ℎ,𝑖 ℎ,𝑋,𝑖 𝜑,ℎ,𝑖

Proof of Theorem opnvonmbllem2 Dummy variables 𝑐 𝑑 𝑒 𝑥 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opnvonmbllem2.x	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ Fin)
2		eqid 2737	. . . . . . . . . . . 12 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
3	2	rrxmetfi 24681	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
4	1, 3	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
5		metxmet 23592	. . . . . . . . . 10 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
7	6	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
8		opnvonmbllem2.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
9		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
10	9	rrxval 24656	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ Fin → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
11	1, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
12	11	fveq2d 6833	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))))
13		ovex 7374	. . . . . . . . . . . . 13 ⊢ (ℝ_fld freeLMod 𝑋) ∈ V
14		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋))
15		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
16		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
17	14, 15, 16	tcphtopn 24495	. . . . . . . . . . . . 13 ⊢ ((ℝ_fld freeLMod 𝑋) ∈ V → (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))))
18	13, 17	ax-mp 5	. . . . . . . . . . . 12 ⊢ (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))))
19	18	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))))
20	11	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ (𝜑 → (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (ℝ^‘𝑋))
21	20	fveq2d 6833	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(ℝ^‘𝑋)))
22	21	fveq2d 6833	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
23	12, 19, 22	3eqtrd 2781	. . . . . . . . . 10 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
24	8, 23	eleqtrd 2840	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
25	24	adantr 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
26		simpr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺)
27		eqid 2737	. . . . . . . . 9 ⊢ (MetOpen‘(dist‘(ℝ^‘𝑋))) = (MetOpen‘(dist‘(ℝ^‘𝑋)))
28	27	mopni2 23754	. . . . . . . 8 ⊢ (((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
29	7, 25, 26, 28	syl3anc 1371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
30	1	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑋 ∈ Fin)
31		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋))
32	31	rrxtoponfi 44220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ Fin → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
33	1, 32	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
34		toponss 22181	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
35	33, 8, 34	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ⊆ (ℝ ↑_m 𝑋))
36	35	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
37	36, 26	sseldd 3936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
38	37	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
39		simpr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ ℝ⁺)
40	30, 38, 39	hoiqssbl 44552	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
41	40	3adant3 1132	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
42		nfv 1917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
43		nfv 1917	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋))
44		nfcv 2905	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑥
45		nfixp1 8781	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
46	44, 45	nfel 2919	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
47		nfcv 2905	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
48	45, 47	nfss 3927	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
49	46, 48	nfan 1902	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
50	42, 43, 49	nf3an 1904	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
51	1	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin)
52	51	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin)
53		elmapi 8712	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℚ ↑_m 𝑋) → 𝑐:𝑋⟶ℚ)
54	53	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑐:𝑋⟶ℚ)
55	54	3ad2ant2 1134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ)
56		elmapi 8712	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (ℚ ↑_m 𝑋) → 𝑑:𝑋⟶ℚ)
57	56	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑑:𝑋⟶ℚ)
58	57	3ad2ant2 1134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ)
59		simp3r 1202	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
60		simp1r 1198	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
61		simp3l 1201	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)))
62		opnvonmbl.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}
63		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩) = (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩)
64	50, 52, 55, 58, 59, 60, 61, 62, 63	opnvonmbllem1 44559	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
65	64	3exp 1119	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
66	65	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
67	66	3adant2 1131	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
68	67	rexlimdvv 3201	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
69	41, 68	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
70	69	3exp 1119	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝑒 ∈ ℝ⁺ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
71	70	rexlimdv 3147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
72	29, 71	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
73		eliun 4949	. . . . . 6 ⊢ (𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
74	72, 73	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
75	74	ralrimiva 3140	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
76		dfss3 3923	. . . 4 ⊢ (𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
77	75, 76	sylibr 233	. . 3 ⊢ (𝜑 → 𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
78	62	eleq2i 2829	. . . . . . . . 9 ⊢ (ℎ ∈ 𝐾 ↔ ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
79	78	biimpi 215	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
80	79	adantl 483	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
81		rabid 3424	. . . . . . 7 ⊢ (ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ↔ (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
82	80, 81	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
83	82	simprd 497	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
84	83	ralrimiva 3140	. . . 4 ⊢ (𝜑 → ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
85		iunss 4996	. . . 4 ⊢ (∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺 ↔ ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
86	84, 85	sylibr 233	. . 3 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
87	77, 86	eqssd 3952	. 2 ⊢ (𝜑 → 𝐺 = ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
88		opnvonmbllem2.n	. . . 4 ⊢ 𝑆 = dom (voln‘𝑋)
89	1, 88	dmovnsal 44539	. . 3 ⊢ (𝜑 → 𝑆 ∈ SAlg)
90		ssrab2 4028	. . . . . 6 ⊢ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ) ↑_m 𝑋)
91	62, 90	eqsstri 3969	. . . . 5 ⊢ 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋)
92	91	a1i 11	. . . 4 ⊢ (𝜑 → 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋))
93		qct 43288	. . . . . . 7 ⊢ ℚ ≼ ω
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → ℚ ≼ ω)
95		xpct 9877	. . . . . 6 ⊢ ((ℚ ≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ) ≼ ω)
96	94, 94, 95	syl2anc 585	. . . . 5 ⊢ (𝜑 → (ℚ × ℚ) ≼ ω)
97	96, 1	mpct 43120	. . . 4 ⊢ (𝜑 → ((ℚ × ℚ) ↑_m 𝑋) ≼ ω)
98		ssct 8920	. . . 4 ⊢ ((𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋) ∧ ((ℚ × ℚ) ↑_m 𝑋) ≼ ω) → 𝐾 ≼ ω)
99	92, 97, 98	syl2anc 585	. . 3 ⊢ (𝜑 → 𝐾 ≼ ω)
100		reex 11067	. . . . . . . . . 10 ⊢ ℝ ∈ V
101	100, 100	xpex 7669	. . . . . . . . 9 ⊢ (ℝ × ℝ) ∈ V
102		qssre 12804	. . . . . . . . . 10 ⊢ ℚ ⊆ ℝ
103		xpss12 5639	. . . . . . . . . 10 ⊢ ((ℚ ⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ) ⊆ (ℝ × ℝ))
104	102, 102, 103	mp2an 690	. . . . . . . . 9 ⊢ (ℚ × ℚ) ⊆ (ℝ × ℝ)
105		mapss 8752	. . . . . . . . 9 ⊢ (((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ) ⊆ (ℝ × ℝ)) → ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋))
106	101, 104, 105	mp2an 690	. . . . . . . 8 ⊢ ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋)
107	91	sseli 3931	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋))
108	106, 107	sselid 3933	. . . . . . 7 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋))
109		elmapi 8712	. . . . . . 7 ⊢ (ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋) → ℎ:𝑋⟶(ℝ × ℝ))
110	108, 109	syl 17	. . . . . 6 ⊢ (ℎ ∈ 𝐾 → ℎ:𝑋⟶(ℝ × ℝ))
111	110	adantl 483	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ:𝑋⟶(ℝ × ℝ))
112		2fveq3 6834	. . . . . 6 ⊢ (𝑘 = 𝑖 → (1^st ‘(ℎ‘𝑘)) = (1^st ‘(ℎ‘𝑖)))
113	112	cbvmptv 5209	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑖)))
114		2fveq3 6834	. . . . . 6 ⊢ (𝑘 = 𝑖 → (2^nd ‘(ℎ‘𝑘)) = (2^nd ‘(ℎ‘𝑖)))
115	114	cbvmptv 5209	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑖)))
116	111, 113, 115	hoicoto2 44532	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) = X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)))
117	1	adantr 482	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → 𝑋 ∈ Fin)
118	111	ffvelcdmda 7021	. . . . . . 7 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑘) ∈ (ℝ × ℝ))
119		xp1st 7935	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
120	118, 119	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
121	120	fmpttd 7049	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))):𝑋⟶ℝ)
122		xp2nd 7936	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
123	118, 122	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
124	123	fmpttd 7049	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))):𝑋⟶ℝ)
125	117, 88, 121, 124	hoimbl 44558	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)) ∈ 𝑆)
126	116, 125	eqeltrd 2838	. . 3 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
127	89, 99, 126	saliuncl 44251	. 2 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
128	87, 127	eqeltrd 2838	1 ⊢ (𝜑 → 𝐺 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3062 ∃wrex 3071 {crab 3404 Vcvv 3442 ⊆ wss 3901 ⟨cop 4583 ∪ ciun 4945 class class class wbr 5096 ↦ cmpt 5179 × cxp 5622 dom cdm 5624 ∘ ccom 5628 ⟶wf 6479 ‘cfv 6483 (class class class)co 7341 ωcom 7784 1^st c1st 7901 2^nd c2nd 7902 ↑_m cmap 8690 Xcixp 8760 ≼ cdom 8806 Fincfn 8808 ℝcr 10975 ℚcq 12793 ℝ⁺crp 12835 [,)cico 13186 distcds 17068 TopOpenctopn 17229 ∞Metcxmet 20687 Metcmet 20688 ballcbl 20689 MetOpencmopn 20692 ℝ_fldcrefld 20914 freeLMod cfrlm 21058 TopOnctopon 22164 toℂPreHilctcph 24436 ℝ^crrx 24652 volncvoln 44465

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5233 ax-sep 5247 ax-nul 5254 ax-pow 5312 ax-pr 5376 ax-un 7654 ax-inf2 9502 ax-cc 10296 ax-ac2 10324 ax-cnex 11032 ax-resscn 11033 ax-1cn 11034 ax-icn 11035 ax-addcl 11036 ax-addrcl 11037 ax-mulcl 11038 ax-mulrcl 11039 ax-mulcom 11040 ax-addass 11041 ax-mulass 11042 ax-distr 11043 ax-i2m1 11044 ax-1ne0 11045 ax-1rid 11046 ax-rnegex 11047 ax-rrecex 11048 ax-cnre 11049 ax-pre-lttri 11050 ax-pre-lttrn 11051 ax-pre-ltadd 11052 ax-pre-mulgt0 11053 ax-pre-sup 11054 ax-addf 11055 ax-mulf 11056

This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3731 df-csb 3847 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3920 df-nul 4274 df-if 4478 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4857 df-int 4899 df-iun 4947 df-iin 4948 df-disj 5062 df-br 5097 df-opab 5159 df-mpt 5180 df-tr 5214 df-id 5522 df-eprel 5528 df-po 5536 df-so 5537 df-fr 5579 df-se 5580 df-we 5581 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6242 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6435 df-fun 6485 df-fn 6486 df-f 6487 df-f1 6488 df-fo 6489 df-f1o 6490 df-fv 6491 df-isom 6492 df-riota 7297 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7599 df-om 7785 df-1st 7903 df-2nd 7904 df-supp 8052 df-tpos 8116 df-frecs 8171 df-wrecs 8202 df-recs 8276 df-rdg 8315 df-1o 8371 df-2o 8372 df-oadd 8375 df-omul 8376 df-er 8573 df-map 8692 df-pm 8693 df-ixp 8761 df-en 8809 df-dom 8810 df-sdom 8811 df-fin 8812 df-fsupp 9231 df-fi 9272 df-sup 9303 df-inf 9304 df-oi 9371 df-dju 9762 df-card 9800 df-acn 9803 df-ac 9977 df-pnf 11116 df-mnf 11117 df-xr 11118 df-ltxr 11119 df-le 11120 df-sub 11312 df-neg 11313 df-div 11738 df-nn 12079 df-2 12141 df-3 12142 df-4 12143 df-5 12144 df-6 12145 df-7 12146 df-8 12147 df-9 12148 df-n0 12339 df-z 12425 df-dec 12543 df-uz 12688 df-q 12794 df-rp 12836 df-xneg 12953 df-xadd 12954 df-xmul 12955 df-ioo 13188 df-ico 13190 df-icc 13191 df-fz 13345 df-fzo 13488 df-fl 13617 df-seq 13827 df-exp 13888 df-hash 14150 df-cj 14909 df-re 14910 df-im 14911 df-sqrt 15045 df-abs 15046 df-clim 15296 df-rlim 15297 df-sum 15497 df-prod 15715 df-struct 16945 df-sets 16962 df-slot 16980 df-ndx 16992 df-base 17010 df-ress 17039 df-plusg 17072 df-mulr 17073 df-starv 17074 df-sca 17075 df-vsca 17076 df-ip 17077 df-tset 17078 df-ple 17079 df-ds 17081 df-unif 17082 df-hom 17083 df-cco 17084 df-rest 17230 df-topn 17231 df-0g 17249 df-gsum 17250 df-topgen 17251 df-prds 17255 df-pws 17257 df-mgm 18423 df-sgrp 18472 df-mnd 18483 df-mhm 18527 df-submnd 18528 df-grp 18676 df-minusg 18677 df-sbg 18678 df-subg 18848 df-ghm 18928 df-cntz 19019 df-cmn 19483 df-abl 19484 df-mgp 19815 df-ur 19832 df-ring 19879 df-cring 19880 df-oppr 19956 df-dvdsr 19977 df-unit 19978 df-invr 20008 df-dvr 20019 df-rnghom 20053 df-drng 20094 df-field 20095 df-subrg 20126 df-abv 20182 df-staf 20210 df-srng 20211 df-lmod 20230 df-lss 20299 df-lmhm 20389 df-lvec 20470 df-sra 20539 df-rgmod 20540 df-psmet 20694 df-xmet 20695 df-met 20696 df-bl 20697 df-mopn 20698 df-cnfld 20703 df-refld 20915 df-phl 20936 df-dsmm 21044 df-frlm 21059 df-top 22148 df-topon 22165 df-topsp 22187 df-bases 22201 df-cmp 22643 df-xms 23578 df-ms 23579 df-nm 23843 df-ngp 23844 df-tng 23845 df-nrg 23846 df-nlm 23847 df-clm 24331 df-cph 24437 df-tcph 24438 df-rrx 24654 df-ovol 24733 df-vol 24734 df-salg 44238 df-sumge0 44290 df-mea 44377 df-ome 44417 df-caragen 44419 df-ovoln 44464 df-voln 44466

This theorem is referenced by: opnvonmbl 44561

W3C validator