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 44061

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 2738	. . . . . . . . . . . 12 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
3	2	rrxmetfi 24481	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
4	1, 3	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
5		metxmet 23395	. . . . . . . . . 10 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
7	6	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
8		opnvonmbllem2.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
9		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
10	9	rrxval 24456	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ Fin → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
11	1, 10	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
12	11	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))))
13		ovex 7288	. . . . . . . . . . . . 13 ⊢ (ℝ_fld freeLMod 𝑋) ∈ V
14		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋))
15		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
16		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
17	14, 15, 16	tcphtopn 24295	. . . . . . . . . . . . 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 2744	. . . . . . . . . . . . 13 ⊢ (𝜑 → (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (ℝ^‘𝑋))
21	20	fveq2d 6760	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(ℝ^‘𝑋)))
22	21	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
23	12, 19, 22	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
24	8, 23	eleqtrd 2841	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
25	24	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
26		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺)
27		eqid 2738	. . . . . . . . 9 ⊢ (MetOpen‘(dist‘(ℝ^‘𝑋))) = (MetOpen‘(dist‘(ℝ^‘𝑋)))
28	27	mopni2 23555	. . . . . . . 8 ⊢ (((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
29	7, 25, 26, 28	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
30	1	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑋 ∈ Fin)
31		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋))
32	31	rrxtoponfi 43722	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ Fin → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
33	1, 32	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
34		toponss 21984	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
35	33, 8, 34	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ⊆ (ℝ ↑_m 𝑋))
36	35	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
37	36, 26	sseldd 3918	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
38	37	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
39		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ ℝ⁺)
40	30, 38, 39	hoiqssbl 44053	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
41	40	3adant3 1130	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
42		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
43		nfv 1918	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋))
44		nfcv 2906	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑥
45		nfixp1 8664	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
46	44, 45	nfel 2920	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
47		nfcv 2906	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
48	45, 47	nfss 3909	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
49	46, 48	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
50	42, 43, 49	nf3an 1905	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
51	1	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin)
52	51	3ad2ant1 1131	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin)
53		elmapi 8595	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℚ ↑_m 𝑋) → 𝑐:𝑋⟶ℚ)
54	53	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑐:𝑋⟶ℚ)
55	54	3ad2ant2 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ)
56		elmapi 8595	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (ℚ ↑_m 𝑋) → 𝑑:𝑋⟶ℚ)
57	56	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑑:𝑋⟶ℚ)
58	57	3ad2ant2 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ)
59		simp3r 1200	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
60		simp1r 1196	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
61		simp3l 1199	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)))
62		opnvonmbl.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}
63		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩) = (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩)
64	50, 52, 55, 58, 59, 60, 61, 62, 63	opnvonmbllem1 44060	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
65	64	3exp 1117	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
66	65	adantlr 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
67	66	3adant2 1129	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
68	67	rexlimdvv 3221	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
69	41, 68	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
70	69	3exp 1117	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝑒 ∈ ℝ⁺ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
71	70	rexlimdv 3211	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
72	29, 71	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
73		eliun 4925	. . . . . 6 ⊢ (𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
74	72, 73	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
75	74	ralrimiva 3107	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
76		dfss3 3905	. . . 4 ⊢ (𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
77	75, 76	sylibr 233	. . 3 ⊢ (𝜑 → 𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
78	62	eleq2i 2830	. . . . . . . . 9 ⊢ (ℎ ∈ 𝐾 ↔ ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
79	78	biimpi 215	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
80	79	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
81		rabid 3304	. . . . . . 7 ⊢ (ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ↔ (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
82	80, 81	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
83	82	simprd 495	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
84	83	ralrimiva 3107	. . . 4 ⊢ (𝜑 → ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
85		iunss 4971	. . . 4 ⊢ (∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺 ↔ ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
86	84, 85	sylibr 233	. . 3 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
87	77, 86	eqssd 3934	. 2 ⊢ (𝜑 → 𝐺 = ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
88		opnvonmbllem2.n	. . . 4 ⊢ 𝑆 = dom (voln‘𝑋)
89	1, 88	dmovnsal 44040	. . 3 ⊢ (𝜑 → 𝑆 ∈ SAlg)
90		ssrab2 4009	. . . . . 6 ⊢ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ) ↑_m 𝑋)
91	62, 90	eqsstri 3951	. . . . 5 ⊢ 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋)
92	91	a1i 11	. . . 4 ⊢ (𝜑 → 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋))
93		qct 42791	. . . . . . 7 ⊢ ℚ ≼ ω
94	93	a1i 11	. . . . . 6 ⊢ (𝜑 → ℚ ≼ ω)
95		xpct 9703	. . . . . 6 ⊢ ((ℚ ≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ) ≼ ω)
96	94, 94, 95	syl2anc 583	. . . . 5 ⊢ (𝜑 → (ℚ × ℚ) ≼ ω)
97	96, 1	mpct 42630	. . . 4 ⊢ (𝜑 → ((ℚ × ℚ) ↑_m 𝑋) ≼ ω)
98		ssct 8793	. . . 4 ⊢ ((𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋) ∧ ((ℚ × ℚ) ↑_m 𝑋) ≼ ω) → 𝐾 ≼ ω)
99	92, 97, 98	syl2anc 583	. . 3 ⊢ (𝜑 → 𝐾 ≼ ω)
100		reex 10893	. . . . . . . . . 10 ⊢ ℝ ∈ V
101	100, 100	xpex 7581	. . . . . . . . 9 ⊢ (ℝ × ℝ) ∈ V
102		qssre 12628	. . . . . . . . . 10 ⊢ ℚ ⊆ ℝ
103		xpss12 5595	. . . . . . . . . 10 ⊢ ((ℚ ⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ) ⊆ (ℝ × ℝ))
104	102, 102, 103	mp2an 688	. . . . . . . . 9 ⊢ (ℚ × ℚ) ⊆ (ℝ × ℝ)
105		mapss 8635	. . . . . . . . 9 ⊢ (((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ) ⊆ (ℝ × ℝ)) → ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋))
106	101, 104, 105	mp2an 688	. . . . . . . 8 ⊢ ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋)
107	91	sseli 3913	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋))
108	106, 107	sselid 3915	. . . . . . 7 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋))
109		elmapi 8595	. . . . . . 7 ⊢ (ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋) → ℎ:𝑋⟶(ℝ × ℝ))
110	108, 109	syl 17	. . . . . 6 ⊢ (ℎ ∈ 𝐾 → ℎ:𝑋⟶(ℝ × ℝ))
111	110	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ:𝑋⟶(ℝ × ℝ))
112		2fveq3 6761	. . . . . 6 ⊢ (𝑘 = 𝑖 → (1^st ‘(ℎ‘𝑘)) = (1^st ‘(ℎ‘𝑖)))
113	112	cbvmptv 5183	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑖)))
114		2fveq3 6761	. . . . . 6 ⊢ (𝑘 = 𝑖 → (2^nd ‘(ℎ‘𝑘)) = (2^nd ‘(ℎ‘𝑖)))
115	114	cbvmptv 5183	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑖)))
116	111, 113, 115	hoicoto2 44033	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) = X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)))
117	1	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → 𝑋 ∈ Fin)
118	111	ffvelrnda 6943	. . . . . . 7 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑘) ∈ (ℝ × ℝ))
119		xp1st 7836	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
120	118, 119	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
121	120	fmpttd 6971	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))):𝑋⟶ℝ)
122		xp2nd 7837	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
123	118, 122	syl 17	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
124	123	fmpttd 6971	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))):𝑋⟶ℝ)
125	117, 88, 121, 124	hoimbl 44059	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)) ∈ 𝑆)
126	116, 125	eqeltrd 2839	. . 3 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
127	89, 99, 126	saliuncl 43753	. 2 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
128	87, 127	eqeltrd 2839	1 ⊢ (𝜑 → 𝐺 ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 {crab 3067 Vcvv 3422 ⊆ wss 3883 ⟨cop 4564 ∪ ciun 4921 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 dom cdm 5580 ∘ ccom 5584 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ωcom 7687 1^st c1st 7802 2^nd c2nd 7803 ↑_m cmap 8573 Xcixp 8643 ≼ cdom 8689 Fincfn 8691 ℝcr 10801 ℚcq 12617 ℝ⁺crp 12659 [,)cico 13010 distcds 16897 TopOpenctopn 17049 ∞Metcxmet 20495 Metcmet 20496 ballcbl 20497 MetOpencmopn 20500 ℝ_fldcrefld 20721 freeLMod cfrlm 20863 TopOnctopon 21967 toℂPreHilctcph 24236 ℝ^crrx 24452 volncvoln 43966

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cc 10122 ax-ac2 10150 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-tpos 8013 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-omul 8272 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-acn 9631 df-ac 9803 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-rlim 15126 df-sum 15326 df-prod 15544 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-prds 17075 df-pws 17077 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-mhm 18345 df-submnd 18346 df-grp 18495 df-minusg 18496 df-sbg 18497 df-subg 18667 df-ghm 18747 df-cntz 18838 df-cmn 19303 df-abl 19304 df-mgp 19636 df-ur 19653 df-ring 19700 df-cring 19701 df-oppr 19777 df-dvdsr 19798 df-unit 19799 df-invr 19829 df-dvr 19840 df-rnghom 19874 df-drng 19908 df-field 19909 df-subrg 19937 df-abv 19992 df-staf 20020 df-srng 20021 df-lmod 20040 df-lss 20109 df-lmhm 20199 df-lvec 20280 df-sra 20349 df-rgmod 20350 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-cnfld 20511 df-refld 20722 df-phl 20743 df-dsmm 20849 df-frlm 20864 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cmp 22446 df-xms 23381 df-ms 23382 df-nm 23644 df-ngp 23645 df-tng 23646 df-nrg 23647 df-nlm 23648 df-clm 24132 df-cph 24237 df-tcph 24238 df-rrx 24454 df-ovol 24533 df-vol 24534 df-salg 43740 df-sumge0 43791 df-mea 43878 df-ome 43918 df-caragen 43920 df-ovoln 43965 df-voln 43967

This theorem is referenced by: opnvonmbl 44062

W3C validator