Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
opnvonmbllem2.n ⊢ 𝑆 = dom ( voln ‘ 𝑋 )
opnvonmbllem2.g ⊢ ( 𝜑 → 𝐺 ∈ ( TopOpen ‘ ( ℝ^ ‘ 𝑋 ) ) )
opnvonmbl.k ⊢ 𝐾 = { ℎ ∈ ( ( ℚ × ℚ ) ↑m 𝑋 ) ∣ X 𝑖 ∈ 𝑋 ( ( [,) ∘ ℎ ) ‘ 𝑖 ) ⊆ 𝐺 }
Assertion opnvonmbllem2 ( 𝜑 → 𝐺 ∈ 𝑆 )

Proof

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