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 42292

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	⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ 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 2772	. . . . . . . . . . . 12 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
3	2	rrxmetfi 23708	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_𝑚 𝑋)))
4	1, 3	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_𝑚 𝑋)))
5		metxmet 22637	. . . . . . . . . 10 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_𝑚 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_𝑚 𝑋)))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_𝑚 𝑋)))
7	6	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_𝑚 𝑋)))
8		opnvonmbllem2.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
9		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
10	9	rrxval 23683	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ Fin → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
11	1, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
12	11	fveq2d 6497	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))))
13		ovex 7002	. . . . . . . . . . . . 13 ⊢ (ℝ_fld freeLMod 𝑋) ∈ V
14		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋))
15		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
16		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
17	14, 15, 16	tcphtopn 23522	. . . . . . . . . . . . 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 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (ℝ^‘𝑋))
21	20	fveq2d 6497	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(ℝ^‘𝑋)))
22	21	fveq2d 6497	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
23	12, 19, 22	3eqtrd 2812	. . . . . . . . . 10 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
24	8, 23	eleqtrd 2862	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
25	24	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
26		simpr 477	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺)
27		eqid 2772	. . . . . . . . 9 ⊢ (MetOpen‘(dist‘(ℝ^‘𝑋))) = (MetOpen‘(dist‘(ℝ^‘𝑋)))
28	27	mopni2 22796	. . . . . . . 8 ⊢ (((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_𝑚 𝑋)) ∧ 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
29	7, 25, 26, 28	syl3anc 1351	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
30	1	ad2antrr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑋 ∈ Fin)
31		eqid 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋))
32	31	rrxtoponfi 41953	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ Fin → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_𝑚 𝑋)))
33	1, 32	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_𝑚 𝑋)))
34		toponss 21229	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_𝑚 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑_𝑚 𝑋))
35	33, 8, 34	syl2anc 576	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ⊆ (ℝ ↑_𝑚 𝑋))
36	35	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ⊆ (ℝ ↑_𝑚 𝑋))
37	36, 26	sseldd 3855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ (ℝ ↑_𝑚 𝑋))
38	37	adantr 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑥 ∈ (ℝ ↑_𝑚 𝑋))
39		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ ℝ⁺)
40	30, 38, 39	hoiqssbl 42284	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑐 ∈ (ℚ ↑_𝑚 𝑋)∃𝑑 ∈ (ℚ ↑_𝑚 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
41	40	3adant3 1112	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑_𝑚 𝑋)∃𝑑 ∈ (ℚ ↑_𝑚 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
42		nfv 1873	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
43		nfv 1873	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋))
44		nfcv 2926	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑥
45		nfixp1 8271	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
46	44, 45	nfel 2938	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
47		nfcv 2926	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
48	45, 47	nfss 3847	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
49	46, 48	nfan 1862	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
50	42, 43, 49	nf3an 1864	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
51	1	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin)
52	51	3ad2ant1 1113	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin)
53		elmapi 8220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) → 𝑐:𝑋⟶ℚ)
54	53	adantr 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) → 𝑐:𝑋⟶ℚ)
55	54	3ad2ant2 1114	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ)
56		elmapi 8220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (ℚ ↑_𝑚 𝑋) → 𝑑:𝑋⟶ℚ)
57	56	adantl 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) → 𝑑:𝑋⟶ℚ)
58	57	3ad2ant2 1114	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ)
59		simp3r 1182	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
60		simp1r 1178	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
61		simp3l 1181	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)))
62		opnvonmbl.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}
63		eqid 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩) = (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩)
64	50, 52, 55, 58, 59, 60, 61, 62, 63	opnvonmbllem1 42291	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
65	64	3exp 1099	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
66	65	adantlr 702	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
67	66	3adant2 1111	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑_𝑚 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
68	67	rexlimdvv 3232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑_𝑚 𝑋)∃𝑑 ∈ (ℚ ↑_𝑚 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
69	41, 68	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
70	69	3exp 1099	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝑒 ∈ ℝ⁺ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
71	70	rexlimdv 3222	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
72	29, 71	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
73		eliun 4790	. . . . . 6 ⊢ (𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
74	72, 73	sylibr 226	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
75	74	ralrimiva 3126	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
76		dfss3 3843	. . . 4 ⊢ (𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
77	75, 76	sylibr 226	. . 3 ⊢ (𝜑 → 𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
78	62	eleq2i 2851	. . . . . . . . 9 ⊢ (ℎ ∈ 𝐾 ↔ ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
79	78	biimpi 208	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
80	79	adantl 474	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
81		rabid 3311	. . . . . . 7 ⊢ (ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ↔ (ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
82	80, 81	sylib 210	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
83	82	simprd 488	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
84	83	ralrimiva 3126	. . . 4 ⊢ (𝜑 → ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
85		iunss 4829	. . . 4 ⊢ (∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺 ↔ ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
86	84, 85	sylibr 226	. . 3 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
87	77, 86	eqssd 3871	. 2 ⊢ (𝜑 → 𝐺 = ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
88		opnvonmbllem2.n	. . . 4 ⊢ 𝑆 = dom (voln‘𝑋)
89	1, 88	dmovnsal 42271	. . 3 ⊢ (𝜑 → 𝑆 ∈ SAlg)
90		ssrab2 3942	. . . . . 6 ⊢ {ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ) ↑_𝑚 𝑋)
91	62, 90	eqsstri 3887	. . . . 5 ⊢ 𝐾 ⊆ ((ℚ × ℚ) ↑_𝑚 𝑋)
92	91	a1i 11	. . . 4 ⊢ (𝜑 → 𝐾 ⊆ ((ℚ × ℚ) ↑_𝑚 𝑋))
93		qct 41005	. . . . . . 7 ⊢ ℚ ≼ ω
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → ℚ ≼ ω)
95		xpct 9228	. . . . . 6 ⊢ ((ℚ ≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ) ≼ ω)
96	94, 94, 95	syl2anc 576	. . . . 5 ⊢ (𝜑 → (ℚ × ℚ) ≼ ω)
97	96, 1	mpct 40835	. . . 4 ⊢ (𝜑 → ((ℚ × ℚ) ↑_𝑚 𝑋) ≼ ω)
98		ssct 8386	. . . 4 ⊢ ((𝐾 ⊆ ((ℚ × ℚ) ↑_𝑚 𝑋) ∧ ((ℚ × ℚ) ↑_𝑚 𝑋) ≼ ω) → 𝐾 ≼ ω)
99	92, 97, 98	syl2anc 576	. . 3 ⊢ (𝜑 → 𝐾 ≼ ω)
100		reex 10418	. . . . . . . . . 10 ⊢ ℝ ∈ V
101	100, 100	xpex 7287	. . . . . . . . 9 ⊢ (ℝ × ℝ) ∈ V
102		qssre 12166	. . . . . . . . . 10 ⊢ ℚ ⊆ ℝ
103		xpss12 5415	. . . . . . . . . 10 ⊢ ((ℚ ⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ) ⊆ (ℝ × ℝ))
104	102, 102, 103	mp2an 679	. . . . . . . . 9 ⊢ (ℚ × ℚ) ⊆ (ℝ × ℝ)
105		mapss 8243	. . . . . . . . 9 ⊢ (((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ) ⊆ (ℝ × ℝ)) → ((ℚ × ℚ) ↑_𝑚 𝑋) ⊆ ((ℝ × ℝ) ↑_𝑚 𝑋))
106	101, 104, 105	mp2an 679	. . . . . . . 8 ⊢ ((ℚ × ℚ) ↑_𝑚 𝑋) ⊆ ((ℝ × ℝ) ↑_𝑚 𝑋)
107	91	sseli 3850	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℚ × ℚ) ↑_𝑚 𝑋))
108	106, 107	sseldi 3852	. . . . . . 7 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℝ × ℝ) ↑_𝑚 𝑋))
109		elmapi 8220	. . . . . . 7 ⊢ (ℎ ∈ ((ℝ × ℝ) ↑_𝑚 𝑋) → ℎ:𝑋⟶(ℝ × ℝ))
110	108, 109	syl 17	. . . . . 6 ⊢ (ℎ ∈ 𝐾 → ℎ:𝑋⟶(ℝ × ℝ))
111	110	adantl 474	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ:𝑋⟶(ℝ × ℝ))
112		2fveq3 6498	. . . . . 6 ⊢ (𝑘 = 𝑖 → (1^st ‘(ℎ‘𝑘)) = (1^st ‘(ℎ‘𝑖)))
113	112	cbvmptv 5022	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑖)))
114		2fveq3 6498	. . . . . 6 ⊢ (𝑘 = 𝑖 → (2^nd ‘(ℎ‘𝑘)) = (2^nd ‘(ℎ‘𝑖)))
115	114	cbvmptv 5022	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑖)))
116	111, 113, 115	hoicoto2 42264	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) = X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)))
117	1	adantr 473	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → 𝑋 ∈ Fin)
118	111	ffvelrnda 6670	. . . . . . 7 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑘) ∈ (ℝ × ℝ))
119		xp1st 7526	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
120	118, 119	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
121	120	fmpttd 6696	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))):𝑋⟶ℝ)
122		xp2nd 7527	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
123	118, 122	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
124	123	fmpttd 6696	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))):𝑋⟶ℝ)
125	117, 88, 121, 124	hoimbl 42290	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)) ∈ 𝑆)
126	116, 125	eqeltrd 2860	. . 3 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
127	89, 99, 126	saliuncl 41984	. 2 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
128	87, 127	eqeltrd 2860	1 ⊢ (𝜑 → 𝐺 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 ∀wral 3082 ∃wrex 3083 {crab 3086 Vcvv 3409 ⊆ wss 3825 ⟨cop 4441 ∪ ciun 4786 class class class wbr 4923 ↦ cmpt 5002 × cxp 5398 dom cdm 5400 ∘ ccom 5404 ⟶wf 6178 ‘cfv 6182 (class class class)co 6970 ωcom 7390 1^st c1st 7492 2^nd c2nd 7493 ↑_𝑚 cmap 8198 Xcixp 8251 ≼ cdom 8296 Fincfn 8298 ℝcr 10326 ℚcq 12155 ℝ⁺crp 12197 [,)cico 12549 distcds 16420 TopOpenctopn 16541 ∞Metcxmet 20222 Metcmet 20223 ballcbl 20224 MetOpencmopn 20227 ℝ_fldcrefld 20440 freeLMod cfrlm 20582 TopOnctopon 21212 toℂPreHilctcph 23464 ℝ^crrx 23679 volncvoln 42197

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-inf2 8890 ax-cc 9647 ax-ac2 9675 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 ax-pre-sup 10405 ax-addf 10406 ax-mulf 10407

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-disj 4892 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-se 5360 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-isom 6191 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-of 7221 df-om 7391 df-1st 7494 df-2nd 7495 df-supp 7627 df-tpos 7688 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-1o 7897 df-2o 7898 df-oadd 7901 df-omul 7902 df-er 8081 df-map 8200 df-pm 8201 df-ixp 8252 df-en 8299 df-dom 8300 df-sdom 8301 df-fin 8302 df-fsupp 8621 df-fi 8662 df-sup 8693 df-inf 8694 df-oi 8761 df-dju 9116 df-card 9154 df-acn 9157 df-ac 9328 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-div 11091 df-nn 11432 df-2 11496 df-3 11497 df-4 11498 df-5 11499 df-6 11500 df-7 11501 df-8 11502 df-9 11503 df-n0 11701 df-z 11787 df-dec 11905 df-uz 12052 df-q 12156 df-rp 12198 df-xneg 12317 df-xadd 12318 df-xmul 12319 df-ioo 12551 df-ico 12553 df-icc 12554 df-fz 12702 df-fzo 12843 df-fl 12970 df-seq 13178 df-exp 13238 df-hash 13499 df-cj 14309 df-re 14310 df-im 14311 df-sqrt 14445 df-abs 14446 df-clim 14696 df-rlim 14697 df-sum 14894 df-prod 15110 df-struct 16331 df-ndx 16332 df-slot 16333 df-base 16335 df-sets 16336 df-ress 16337 df-plusg 16424 df-mulr 16425 df-starv 16426 df-sca 16427 df-vsca 16428 df-ip 16429 df-tset 16430 df-ple 16431 df-ds 16433 df-unif 16434 df-hom 16435 df-cco 16436 df-rest 16542 df-topn 16543 df-0g 16561 df-gsum 16562 df-topgen 16563 df-prds 16567 df-pws 16569 df-mgm 17700 df-sgrp 17742 df-mnd 17753 df-mhm 17793 df-submnd 17794 df-grp 17884 df-minusg 17885 df-sbg 17886 df-subg 18050 df-ghm 18117 df-cntz 18208 df-cmn 18658 df-abl 18659 df-mgp 18953 df-ur 18965 df-ring 19012 df-cring 19013 df-oppr 19086 df-dvdsr 19104 df-unit 19105 df-invr 19135 df-dvr 19146 df-rnghom 19180 df-drng 19217 df-field 19218 df-subrg 19246 df-abv 19300 df-staf 19328 df-srng 19329 df-lmod 19348 df-lss 19416 df-lmhm 19506 df-lvec 19587 df-sra 19656 df-rgmod 19657 df-psmet 20229 df-xmet 20230 df-met 20231 df-bl 20232 df-mopn 20233 df-cnfld 20238 df-refld 20441 df-phl 20462 df-dsmm 20568 df-frlm 20583 df-top 21196 df-topon 21213 df-topsp 21235 df-bases 21248 df-cmp 21689 df-xms 22623 df-ms 22624 df-nm 22885 df-ngp 22886 df-tng 22887 df-nrg 22888 df-nlm 22889 df-clm 23360 df-cph 23465 df-tcph 23466 df-rrx 23681 df-ovol 23758 df-vol 23759 df-salg 41971 df-sumge0 42022 df-mea 42109 df-ome 42149 df-caragen 42151 df-ovoln 42196 df-voln 42198

This theorem is referenced by: opnvonmbl 42293

W3C validator