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 47779

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 2760	. . . . . . . . . . . 12 ⊢ (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
3	2	rrxmetfi 25742	. . . . . . . . . . 11 ⊢ (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
4	1, 3	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)))
5		metxmet 24662	. . . . . . . . . 10 ⊢ ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑_m 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
6	4, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
7	6	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)))
8		opnvonmbllem2.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
9		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (ℝ^‘𝑋) = (ℝ^‘𝑋)
10	9	rrxval 25717	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ Fin → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
11	1, 10	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (ℝ^‘𝑋) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
12	11	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))))
13		ovex 7457	. . . . . . . . . . . . 13 ⊢ (ℝ_fld freeLMod 𝑋) ∈ V
14		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (toℂPreHil‘(ℝ_fld freeLMod 𝑋))
15		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
16		eqid 2760	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (TopOpen‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))
17	14, 15, 16	tcphtopn 25556	. . . . . . . . . . . . 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 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → (toℂPreHil‘(ℝ_fld freeLMod 𝑋)) = (ℝ^‘𝑋))
21	20	fveq2d 6894	. . . . . . . . . . . 12 ⊢ (𝜑 → (dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋))) = (dist‘(ℝ^‘𝑋)))
22	21	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝜑 → (MetOpen‘(dist‘(toℂPreHil‘(ℝ_fld freeLMod 𝑋)))) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
23	12, 19, 22	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
24	8, 23	eleqtrd 2862	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
25	24	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
26		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺)
27		eqid 2760	. . . . . . . . 9 ⊢ (MetOpen‘(dist‘(ℝ^‘𝑋))) = (MetOpen‘(dist‘(ℝ^‘𝑋)))
28	27	mopni2 24821	. . . . . . . 8 ⊢ (((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
29	7, 25, 26, 28	syl3anc 1398	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
30	1	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑋 ∈ Fin)
31		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋))
32	31	rrxtoponfi 47437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ Fin → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
33	1, 32	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)))
34		toponss 23254	. . . . . . . . . . . . . . . 16 ⊢ (((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑_m 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
35	33, 8, 34	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺 ⊆ (ℝ ↑_m 𝑋))
36	35	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ⊆ (ℝ ↑_m 𝑋))
37	36, 26	sseldd 3910	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
38	37	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑥 ∈ (ℝ ↑_m 𝑋))
39		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → 𝑒 ∈ ℝ⁺)
40	30, 38, 39	hoiqssbl 47771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
41	40	3adant3 1150	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
42		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
43		nfv 1946	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋))
44		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖𝑥
45		nfixp1 8954	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
46	44, 45	nfel 2936	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))
47		nfcv 2922	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
48	45, 47	nfss 3902	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
49	46, 48	nfan 1931	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑖(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
50	42, 43, 49	nf3an 1933	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
51	1	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin)
52	51	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin)
53		elmapi 8877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (ℚ ↑_m 𝑋) → 𝑐:𝑋⟶ℚ)
54	53	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑐:𝑋⟶ℚ)
55	54	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ)
56		elmapi 8877	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (ℚ ↑_m 𝑋) → 𝑑:𝑋⟶ℚ)
57	56	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → 𝑑:𝑋⟶ℚ)
58	57	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ)
59		simp3r 1221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
60		simp1r 1217	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
61		simp3l 1220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)))
62		opnvonmbl.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}
63		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩) = (𝑖 ∈ 𝑋 ↦ ⟨(𝑐‘𝑖), (𝑑‘𝑖)⟩)
64	50, 52, 55, 58, 59, 60, 61, 62, 63	opnvonmbllem1 47778	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) ∧ (𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
65	64	3exp 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
66	65	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
67	66	3adant2 1149	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑_m 𝑋) ∧ 𝑑 ∈ (ℚ ↑_m 𝑋)) → ((𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
68	67	rexlimdvv 3218	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑_m 𝑋)∃𝑑 ∈ (ℚ ↑_m 𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
69	41, 68	mpd 16	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ⁺ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
70	69	3exp 1137	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝑒 ∈ ℝ⁺ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))))
71	70	rexlimdv 3161	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑒 ∈ ℝ⁺ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))
72	29, 71	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
73		eliun 4954	. . . . . 6 ⊢ (𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
74	72, 73	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
75	74	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
76		dfss3 3898	. . . 4 ⊢ (𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
77	75, 76	sylibr 237	. . 3 ⊢ (𝜑 → 𝐺 ⊆ ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
78	62	eleq2i 2852	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 ↔ ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
79	78	bilani 510	. . . . . . 7 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺})
80		rabid 3432	. . . . . . 7 ⊢ (ℎ ∈ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ↔ (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
81	79, 80	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺))
82	81	simprd 501	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
83	82	ralrimiva 3154	. . . 4 ⊢ (𝜑 → ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
84		iunss 5002	. . . 4 ⊢ (∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺 ↔ ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
85	83, 84	sylibr 237	. . 3 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)
86	77, 85	eqssd 3926	. 2 ⊢ (𝜑 → 𝐺 = ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))
87		opnvonmbllem2.n	. . . 4 ⊢ 𝑆 = dom (voln‘𝑋)
88	1, 87	dmovnsal 47758	. . 3 ⊢ (𝜑 → 𝑆 ∈ SAlg)
89		ssrab2 4004	. . . . . 6 ⊢ {ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ) ↑_m 𝑋)
90	62, 89	eqsstri 3955	. . . . 5 ⊢ 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋)
91	90	a1i 11	. . . 4 ⊢ (𝜑 → 𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋))
92		qct 46510	. . . . . . 7 ⊢ ℚ ≼ ω
93	92	a1i 11	. . . . . 6 ⊢ (𝜑 → ℚ ≼ ω)
94		xpct 10102	. . . . . 6 ⊢ ((ℚ ≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ) ≼ ω)
95	93, 93, 94	syl2anc 596	. . . . 5 ⊢ (𝜑 → (ℚ × ℚ) ≼ ω)
96	95, 1	mpct 46351	. . . 4 ⊢ (𝜑 → ((ℚ × ℚ) ↑_m 𝑋) ≼ ω)
97		ssct 9085	. . . 4 ⊢ ((𝐾 ⊆ ((ℚ × ℚ) ↑_m 𝑋) ∧ ((ℚ × ℚ) ↑_m 𝑋) ≼ ω) → 𝐾 ≼ ω)
98	91, 96, 97	syl2anc 596	. . 3 ⊢ (𝜑 → 𝐾 ≼ ω)
99		reex 11298	. . . . . . . . . 10 ⊢ ℝ ∈ V
100	99, 99	xpex 7771	. . . . . . . . 9 ⊢ (ℝ × ℝ) ∈ V
101		qssre 13093	. . . . . . . . . 10 ⊢ ℚ ⊆ ℝ
102		xpss12 5666	. . . . . . . . . 10 ⊢ ((ℚ ⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ) ⊆ (ℝ × ℝ))
103	101, 101, 102	mp2an 705	. . . . . . . . 9 ⊢ (ℚ × ℚ) ⊆ (ℝ × ℝ)
104		mapss 8925	. . . . . . . . 9 ⊢ (((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ) ⊆ (ℝ × ℝ)) → ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋))
105	100, 103, 104	mp2an 705	. . . . . . . 8 ⊢ ((ℚ × ℚ) ↑_m 𝑋) ⊆ ((ℝ × ℝ) ↑_m 𝑋)
106	90	sseli 3905	. . . . . . . 8 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℚ × ℚ) ↑_m 𝑋))
107	105, 106	sselid 3907	. . . . . . 7 ⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋))
108		elmapi 8877	. . . . . . 7 ⊢ (ℎ ∈ ((ℝ × ℝ) ↑_m 𝑋) → ℎ:𝑋⟶(ℝ × ℝ))
109	107, 108	syl 18	. . . . . 6 ⊢ (ℎ ∈ 𝐾 → ℎ:𝑋⟶(ℝ × ℝ))
110	109	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ:𝑋⟶(ℝ × ℝ))
111		2fveq3 6895	. . . . . 6 ⊢ (𝑘 = 𝑖 → (1^st ‘(ℎ‘𝑘)) = (1^st ‘(ℎ‘𝑖)))
112	111	cbvmptv 5208	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑖)))
113		2fveq3 6895	. . . . . 6 ⊢ (𝑘 = 𝑖 → (2^nd ‘(ℎ‘𝑘)) = (2^nd ‘(ℎ‘𝑖)))
114	113	cbvmptv 5208	. . . . 5 ⊢ (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑖)))
115	110, 112, 114	hoicoto2 47751	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) = X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)))
116	1	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → 𝑋 ∈ Fin)
117	110	ffvelcdmda 7089	. . . . . . 7 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑘) ∈ (ℝ × ℝ))
118		xp1st 8037	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
119	117, 118	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (1^st ‘(ℎ‘𝑘)) ∈ ℝ)
120	119	fmpttd 7120	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘))):𝑋⟶ℝ)
121		xp2nd 8038	. . . . . . 7 ⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
122	117, 121	syl 18	. . . . . 6 ⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (2^nd ‘(ℎ‘𝑘)) ∈ ℝ)
123	122	fmpttd 7120	. . . . 5 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘))):𝑋⟶ℝ)
124	116, 87, 120, 123	hoimbl 47777	. . . 4 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1^st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2^nd ‘(ℎ‘𝑘)))‘𝑖)) ∈ 𝑆)
125	115, 124	eqeltrd 2860	. . 3 ⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
126	88, 98, 125	saliuncl 47469	. 2 ⊢ (𝜑 → ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆)
127	86, 126	eqeltrd 2860	1 ⊢ (𝜑 → 𝐺 ∈ 𝑆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3896 ⟨cop 4834 ∪ ciun 4950 class class class wbr 5102 ↦ cmpt 5185 × cxp 5649 dom cdm 5651 ∘ ccom 5655 ⟶wf 6539 ‘cfv 6543 (class class class)co 7424 ωcom 7881 1^st c1st 8003 2^nd c2nd 8004 ↑_m cmap 8855 Xcixp 8933 ≼ cdom 8979 Fincfn 8981 ℝcr 11206 ℚcq 13082 ℝ⁺crp 13127 [,)cico 13485 distcds 17446 TopOpenctopn 17601 ∞Metcxmet 21672 Metcmet 21673 ballcbl 21674 MetOpencmopn 21677 ℝ_fldcrefld 21919 freeLMod cfrlm 22061 TopOnctopon 23237 toℂPreHilctcph 25497 ℝ^crrx 25713 volncvoln 47684

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-inf2 9649 ax-cc 10520 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284 ax-pre-sup 11285 ax-addf 11286 ax-mulf 11287

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-of 7697 df-om 7882 df-1st 8005 df-2nd 8006 df-supp 8185 df-tpos 8251 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-2o 8485 df-oadd 8488 df-omul 8489 df-er 8725 df-map 8857 df-pm 8858 df-ixp 8934 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-fsupp 9362 df-fi 9410 df-sup 9441 df-inf 9442 df-oi 9511 df-dju 9989 df-card 10027 df-acn 10030 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-div 11981 df-nn 12343 df-2 12412 df-3 12413 df-4 12414 df-5 12415 df-6 12416 df-7 12417 df-8 12418 df-9 12419 df-n0 12614 df-z 12701 df-dec 12822 df-uz 12973 df-q 13083 df-rp 13128 df-xneg 13248 df-xadd 13249 df-xmul 13250 df-ioo 13487 df-ico 13489 df-icc 13490 df-fz 13647 df-fzo 13796 df-fl 13939 df-seq 14152 df-exp 14212 df-hash 14482 df-cj 15275 df-re 15276 df-im 15277 df-sqrt 15411 df-abs 15412 df-clim 15664 df-rlim 15665 df-sum 15863 df-prod 16082 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-mulr 17451 df-starv 17452 df-sca 17453 df-vsca 17454 df-ip 17455 df-tset 17456 df-ple 17457 df-ds 17459 df-unif 17460 df-hom 17461 df-cco 17462 df-rest 17602 df-topn 17603 df-0g 17621 df-gsum 17622 df-topgen 17623 df-prds 17627 df-pws 17629 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-mhm 18987 df-submnd 18988 df-grp 19156 df-minusg 19157 df-sbg 19158 df-subg 19342 df-ghm 19437 df-cntz 19540 df-cmn 20005 df-abl 20006 df-mgp 20370 df-rng 20384 df-ur 20417 df-ring 20470 df-cring 20471 df-oppr 20576 df-dvdsr 20596 df-unit 20597 df-invr 20627 df-dvr 20640 df-rhm 20711 df-subrng 20807 df-subrg 20831 df-drng 20991 df-field 20992 df-abv 21075 df-staf 21105 df-srng 21106 df-lmod 21146 df-lss 21216 df-lmhm 21306 df-lvec 21387 df-sra 21457 df-rgmod 21458 df-psmet 21679 df-xmet 21680 df-met 21681 df-bl 21682 df-mopn 21683 df-cnfld 21688 df-refld 21920 df-phl 21941 df-dsmm 22047 df-frlm 22062 df-top 23221 df-topon 23238 df-topsp 23260 df-bases 23273 df-cmp 23714 df-xms 24648 df-ms 24649 df-nm 24910 df-ngp 24911 df-tng 24912 df-nrg 24913 df-nlm 24914 df-clm 25393 df-cph 25498 df-tcph 25499 df-rrx 25715 df-ovol 25794 df-vol 25795 df-salg 47455 df-sumge0 47509 df-mea 47596 df-ome 47636 df-caragen 47638 df-ovoln 47683 df-voln 47685

This theorem is used by: opnvonmbl 47780

W3C validator