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

Theorem opnvonmbllem2 39322
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.
StepHypRef Expression
1 opnvonmbllem2.x . . . . . . . . . . 11 (𝜑𝑋 ∈ Fin)
2 eqid 2604 . . . . . . . . . . . 12 (dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋))
32rrxmetfi 38982 . . . . . . . . . . 11 (𝑋 ∈ Fin → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑𝑚 𝑋)))
41, 3syl 17 . . . . . . . . . 10 (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑𝑚 𝑋)))
5 metxmet 21885 . . . . . . . . . 10 ((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ ↑𝑚 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑𝑚 𝑋)))
64, 5syl 17 . . . . . . . . 9 (𝜑 → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑𝑚 𝑋)))
76adantr 479 . . . . . . . 8 ((𝜑𝑥𝐺) → (dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑𝑚 𝑋)))
8 opnvonmbllem2.g . . . . . . . . . 10 (𝜑𝐺 ∈ (TopOpen‘(ℝ^‘𝑋)))
9 eqid 2604 . . . . . . . . . . . . . 14 (ℝ^‘𝑋) = (ℝ^‘𝑋)
109rrxval 22895 . . . . . . . . . . . . 13 (𝑋 ∈ Fin → (ℝ^‘𝑋) = (toℂHil‘(ℝfld freeLMod 𝑋)))
111, 10syl 17 . . . . . . . . . . . 12 (𝜑 → (ℝ^‘𝑋) = (toℂHil‘(ℝfld freeLMod 𝑋)))
1211fveq2d 6087 . . . . . . . . . . 11 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))))
13 ovex 6550 . . . . . . . . . . . . 13 (ℝfld freeLMod 𝑋) ∈ V
14 eqid 2604 . . . . . . . . . . . . . 14 (toℂHil‘(ℝfld freeLMod 𝑋)) = (toℂHil‘(ℝfld freeLMod 𝑋))
15 eqid 2604 . . . . . . . . . . . . . 14 (dist‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (dist‘(toℂHil‘(ℝfld freeLMod 𝑋)))
16 eqid 2604 . . . . . . . . . . . . . 14 (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋)))
1714, 15, 16tchtopn 22749 . . . . . . . . . . . . 13 ((ℝfld freeLMod 𝑋) ∈ V → (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod 𝑋)))))
1813, 17ax-mp 5 . . . . . . . . . . . 12 (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod 𝑋))))
1918a1i 11 . . . . . . . . . . 11 (𝜑 → (TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod 𝑋)))))
2011eqcomd 2610 . . . . . . . . . . . . 13 (𝜑 → (toℂHil‘(ℝfld freeLMod 𝑋)) = (ℝ^‘𝑋))
2120fveq2d 6087 . . . . . . . . . . . 12 (𝜑 → (dist‘(toℂHil‘(ℝfld freeLMod 𝑋))) = (dist‘(ℝ^‘𝑋)))
2221fveq2d 6087 . . . . . . . . . . 11 (𝜑 → (MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod 𝑋)))) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
2312, 19, 223eqtrd 2642 . . . . . . . . . 10 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) = (MetOpen‘(dist‘(ℝ^‘𝑋))))
248, 23eleqtrd 2684 . . . . . . . . 9 (𝜑𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
2524adantr 479 . . . . . . . 8 ((𝜑𝑥𝐺) → 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))))
26 simpr 475 . . . . . . . 8 ((𝜑𝑥𝐺) → 𝑥𝐺)
27 eqid 2604 . . . . . . . . 9 (MetOpen‘(dist‘(ℝ^‘𝑋))) = (MetOpen‘(dist‘(ℝ^‘𝑋)))
2827mopni2 22044 . . . . . . . 8 (((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ ↑𝑚 𝑋)) ∧ 𝐺 ∈ (MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥𝐺) → ∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
297, 25, 26, 28syl3anc 1317 . . . . . . 7 ((𝜑𝑥𝐺) → ∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
301ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ Fin)
31 eqid 2604 . . . . . . . . . . . . . . . . . 18 (TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋))
3231rrxtoponfi 38986 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ Fin → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑𝑚 𝑋)))
331, 32syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑𝑚 𝑋)))
34 toponss 20481 . . . . . . . . . . . . . . . 16 (((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ ↑𝑚 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑𝑚 𝑋))
3533, 8, 34syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑𝐺 ⊆ (ℝ ↑𝑚 𝑋))
3635adantr 479 . . . . . . . . . . . . . 14 ((𝜑𝑥𝐺) → 𝐺 ⊆ (ℝ ↑𝑚 𝑋))
3736, 26sseldd 3563 . . . . . . . . . . . . 13 ((𝜑𝑥𝐺) → 𝑥 ∈ (ℝ ↑𝑚 𝑋))
3837adantr 479 . . . . . . . . . . . 12 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑥 ∈ (ℝ ↑𝑚 𝑋))
39 simpr 475 . . . . . . . . . . . 12 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈ ℝ+)
4030, 38, 39hoiqssbl 39314 . . . . . . . . . . 11 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+) → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
41403adant3 1073 . . . . . . . . . 10 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
42 nfv 1828 . . . . . . . . . . . . . . . 16 𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
43 nfv 1828 . . . . . . . . . . . . . . . 16 𝑖(𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋))
44 nfcv 2745 . . . . . . . . . . . . . . . . . 18 𝑖𝑥
45 nfixp1 7786 . . . . . . . . . . . . . . . . . 18 𝑖X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖))
4644, 45nfel 2757 . . . . . . . . . . . . . . . . 17 𝑖 𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖))
47 nfcv 2745 . . . . . . . . . . . . . . . . . 18 𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
4845, 47nfss 3555 . . . . . . . . . . . . . . . . 17 𝑖X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)
4946, 48nfan 1814 . . . . . . . . . . . . . . . 16 𝑖(𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
5042, 43, 49nf3an 1817 . . . . . . . . . . . . . . 15 𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)))
511adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin)
52513ad2ant1 1074 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin)
53 elmapi 7737 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ (ℚ ↑𝑚 𝑋) → 𝑐:𝑋⟶ℚ)
5453adantr 479 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → 𝑐:𝑋⟶ℚ)
55543ad2ant2 1075 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ)
56 elmapi 7737 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (ℚ ↑𝑚 𝑋) → 𝑑:𝑋⟶ℚ)
5756adantl 480 . . . . . . . . . . . . . . . 16 ((𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → 𝑑:𝑋⟶ℚ)
58573ad2ant2 1075 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ)
59 simp3r 1082 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))
60 simp1r 1078 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺)
61 simp3l 1081 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)))
62 opnvonmbl.k . . . . . . . . . . . . . . 15 𝐾 = { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺}
63 eqid 2604 . . . . . . . . . . . . . . 15 (𝑖𝑋 ↦ ⟨(𝑐𝑖), (𝑑𝑖)⟩) = (𝑖𝑋 ↦ ⟨(𝑐𝑖), (𝑑𝑖)⟩)
6450, 52, 55, 58, 59, 60, 61, 62, 63opnvonmbllem1 39321 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) ∧ (𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))
65643exp 1255 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → ((𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))))
6665adantlr 746 . . . . . . . . . . . 12 (((𝜑𝑥𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → ((𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))))
67663adant2 1072 . . . . . . . . . . 11 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚 𝑋)) → ((𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))))
6867rexlimdvv 3013 . . . . . . . . . 10 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚 𝑋)(𝑥X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ∧ X𝑖𝑋 ((𝑐𝑖)[,)(𝑑𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖)))
6941, 68mpd 15 . . . . . . . . 9 (((𝜑𝑥𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))
70693exp 1255 . . . . . . . 8 ((𝜑𝑥𝐺) → (𝑒 ∈ ℝ+ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))))
7170rexlimdv 3006 . . . . . . 7 ((𝜑𝑥𝐺) → (∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖)))
7229, 71mpd 15 . . . . . 6 ((𝜑𝑥𝐺) → ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))
73 eliun 4449 . . . . . 6 (𝑥 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ↔ ∃𝐾 𝑥X𝑖𝑋 (([,) ∘ )‘𝑖))
7472, 73sylibr 222 . . . . 5 ((𝜑𝑥𝐺) → 𝑥 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖))
7574ralrimiva 2943 . . . 4 (𝜑 → ∀𝑥𝐺 𝑥 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖))
76 dfss3 3552 . . . 4 (𝐺 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ↔ ∀𝑥𝐺 𝑥 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖))
7775, 76sylibr 222 . . 3 (𝜑𝐺 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖))
7862eleq2i 2674 . . . . . . . . 9 (𝐾 ∈ { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺})
7978biimpi 204 . . . . . . . 8 (𝐾 ∈ { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺})
8079adantl 480 . . . . . . 7 ((𝜑𝐾) → ∈ { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺})
81 rabid 3089 . . . . . . 7 ( ∈ { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺} ↔ ( ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∧ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺))
8280, 81sylib 206 . . . . . 6 ((𝜑𝐾) → ( ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∧ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺))
8382simprd 477 . . . . 5 ((𝜑𝐾) → X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺)
8483ralrimiva 2943 . . . 4 (𝜑 → ∀𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺)
85 iunss 4486 . . . 4 ( 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺 ↔ ∀𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺)
8684, 85sylibr 222 . . 3 (𝜑 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺)
8777, 86eqssd 3579 . 2 (𝜑𝐺 = 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖))
88 opnvonmbllem2.n . . . 4 𝑆 = dom (voln‘𝑋)
891, 88dmovnsal 39301 . . 3 (𝜑𝑆 ∈ SAlg)
90 ssrab2 3644 . . . . . 6 { ∈ ((ℚ × ℚ) ↑𝑚 𝑋) ∣ X𝑖𝑋 (([,) ∘ )‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ) ↑𝑚 𝑋)
9162, 90eqsstri 3592 . . . . 5 𝐾 ⊆ ((ℚ × ℚ) ↑𝑚 𝑋)
9291a1i 11 . . . 4 (𝜑𝐾 ⊆ ((ℚ × ℚ) ↑𝑚 𝑋))
93 qct 38318 . . . . . . 7 ℚ ≼ ω
9493a1i 11 . . . . . 6 (𝜑 → ℚ ≼ ω)
95 xpct 8694 . . . . . 6 ((ℚ ≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ) ≼ ω)
9694, 94, 95syl2anc 690 . . . . 5 (𝜑 → (ℚ × ℚ) ≼ ω)
9796, 1mpct 38186 . . . 4 (𝜑 → ((ℚ × ℚ) ↑𝑚 𝑋) ≼ ω)
98 ssct 7898 . . . 4 ((𝐾 ⊆ ((ℚ × ℚ) ↑𝑚 𝑋) ∧ ((ℚ × ℚ) ↑𝑚 𝑋) ≼ ω) → 𝐾 ≼ ω)
9992, 97, 98syl2anc 690 . . 3 (𝜑𝐾 ≼ ω)
100 reex 9878 . . . . . . . . . 10 ℝ ∈ V
101100, 100xpex 6832 . . . . . . . . 9 (ℝ × ℝ) ∈ V
102 qssre 11625 . . . . . . . . . 10 ℚ ⊆ ℝ
103 xpss12 5132 . . . . . . . . . 10 ((ℚ ⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ) ⊆ (ℝ × ℝ))
104102, 102, 103mp2an 703 . . . . . . . . 9 (ℚ × ℚ) ⊆ (ℝ × ℝ)
105 mapss 7758 . . . . . . . . 9 (((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ) ⊆ (ℝ × ℝ)) → ((ℚ × ℚ) ↑𝑚 𝑋) ⊆ ((ℝ × ℝ) ↑𝑚 𝑋))
106101, 104, 105mp2an 703 . . . . . . . 8 ((ℚ × ℚ) ↑𝑚 𝑋) ⊆ ((ℝ × ℝ) ↑𝑚 𝑋)
10791sseli 3558 . . . . . . . 8 (𝐾 ∈ ((ℚ × ℚ) ↑𝑚 𝑋))
108106, 107sseldi 3560 . . . . . . 7 (𝐾 ∈ ((ℝ × ℝ) ↑𝑚 𝑋))
109 elmapi 7737 . . . . . . 7 ( ∈ ((ℝ × ℝ) ↑𝑚 𝑋) → :𝑋⟶(ℝ × ℝ))
110108, 109syl 17 . . . . . 6 (𝐾:𝑋⟶(ℝ × ℝ))
111110adantl 480 . . . . 5 ((𝜑𝐾) → :𝑋⟶(ℝ × ℝ))
112 fveq2 6083 . . . . . . 7 (𝑘 = 𝑖 → (𝑘) = (𝑖))
113112fveq2d 6087 . . . . . 6 (𝑘 = 𝑖 → (1st ‘(𝑘)) = (1st ‘(𝑖)))
114113cbvmptv 4667 . . . . 5 (𝑘𝑋 ↦ (1st ‘(𝑘))) = (𝑖𝑋 ↦ (1st ‘(𝑖)))
115112fveq2d 6087 . . . . . 6 (𝑘 = 𝑖 → (2nd ‘(𝑘)) = (2nd ‘(𝑖)))
116115cbvmptv 4667 . . . . 5 (𝑘𝑋 ↦ (2nd ‘(𝑘))) = (𝑖𝑋 ↦ (2nd ‘(𝑖)))
117111, 114, 116hoicoto2 39294 . . . 4 ((𝜑𝐾) → X𝑖𝑋 (([,) ∘ )‘𝑖) = X𝑖𝑋 (((𝑘𝑋 ↦ (1st ‘(𝑘)))‘𝑖)[,)((𝑘𝑋 ↦ (2nd ‘(𝑘)))‘𝑖)))
1181adantr 479 . . . . 5 ((𝜑𝐾) → 𝑋 ∈ Fin)
119111ffvelrnda 6247 . . . . . . 7 (((𝜑𝐾) ∧ 𝑘𝑋) → (𝑘) ∈ (ℝ × ℝ))
120 xp1st 7061 . . . . . . 7 ((𝑘) ∈ (ℝ × ℝ) → (1st ‘(𝑘)) ∈ ℝ)
121119, 120syl 17 . . . . . 6 (((𝜑𝐾) ∧ 𝑘𝑋) → (1st ‘(𝑘)) ∈ ℝ)
122 eqid 2604 . . . . . 6 (𝑘𝑋 ↦ (1st ‘(𝑘))) = (𝑘𝑋 ↦ (1st ‘(𝑘)))
123121, 122fmptd 6272 . . . . 5 ((𝜑𝐾) → (𝑘𝑋 ↦ (1st ‘(𝑘))):𝑋⟶ℝ)
124 xp2nd 7062 . . . . . . 7 ((𝑘) ∈ (ℝ × ℝ) → (2nd ‘(𝑘)) ∈ ℝ)
125119, 124syl 17 . . . . . 6 (((𝜑𝐾) ∧ 𝑘𝑋) → (2nd ‘(𝑘)) ∈ ℝ)
126 eqid 2604 . . . . . 6 (𝑘𝑋 ↦ (2nd ‘(𝑘))) = (𝑘𝑋 ↦ (2nd ‘(𝑘)))
127125, 126fmptd 6272 . . . . 5 ((𝜑𝐾) → (𝑘𝑋 ↦ (2nd ‘(𝑘))):𝑋⟶ℝ)
128118, 88, 123, 127hoimbl 39320 . . . 4 ((𝜑𝐾) → X𝑖𝑋 (((𝑘𝑋 ↦ (1st ‘(𝑘)))‘𝑖)[,)((𝑘𝑋 ↦ (2nd ‘(𝑘)))‘𝑖)) ∈ 𝑆)
129117, 128eqeltrd 2682 . . 3 ((𝜑𝐾) → X𝑖𝑋 (([,) ∘ )‘𝑖) ∈ 𝑆)
13089, 99, 129saliuncl 39017 . 2 (𝜑 𝐾 X𝑖𝑋 (([,) ∘ )‘𝑖) ∈ 𝑆)
13187, 130eqeltrd 2682 1 (𝜑𝐺𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1975  wral 2890  wrex 2891  {crab 2894  Vcvv 3167  wss 3534  cop 4125   ciun 4444   class class class wbr 4572  cmpt 4632   × cxp 5021  dom cdm 5023  ccom 5027  wf 5781  cfv 5785  (class class class)co 6522  ωcom 6929  1st c1st 7029  2nd c2nd 7030  𝑚 cmap 7716  Xcixp 7766  cdom 7811  Fincfn 7813  cr 9786  cq 11615  +crp 11659  [,)cico 11999  distcds 15718  TopOpenctopn 15846  ∞Metcxmt 19493  Metcme 19494  ballcbl 19495  MetOpencmopn 19498  fldcrefld 19709   freeLMod cfrlm 19846  TopOnctopon 20455  toℂHilctch 22694  ℝ^crrx 22891  volncvoln 39227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-rep 4688  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-inf2 8393  ax-cc 9112  ax-ac2 9140  ax-cnex 9843  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-mulcom 9851  ax-addass 9852  ax-mulass 9853  ax-distr 9854  ax-i2m1 9855  ax-1ne0 9856  ax-1rid 9857  ax-rnegex 9858  ax-rrecex 9859  ax-cnre 9860  ax-pre-lttri 9861  ax-pre-lttrn 9862  ax-pre-ltadd 9863  ax-pre-mulgt0 9864  ax-pre-sup 9865  ax-addf 9866  ax-mulf 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-reu 2897  df-rmo 2898  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-pss 3550  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-tp 4124  df-op 4126  df-uni 4362  df-int 4400  df-iun 4446  df-iin 4447  df-disj 4543  df-br 4573  df-opab 4633  df-mpt 4634  df-tr 4670  df-eprel 4934  df-id 4938  df-po 4944  df-so 4945  df-fr 4982  df-se 4983  df-we 4984  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-pred 5578  df-ord 5624  df-on 5625  df-lim 5626  df-suc 5627  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-isom 5794  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-of 6767  df-om 6930  df-1st 7031  df-2nd 7032  df-supp 7155  df-tpos 7211  df-wrecs 7266  df-recs 7327  df-rdg 7365  df-1o 7419  df-2o 7420  df-oadd 7423  df-omul 7424  df-er 7601  df-map 7718  df-pm 7719  df-ixp 7767  df-en 7814  df-dom 7815  df-sdom 7816  df-fin 7817  df-fsupp 8131  df-fi 8172  df-sup 8203  df-inf 8204  df-oi 8270  df-card 8620  df-acn 8623  df-ac 8794  df-cda 8845  df-pnf 9927  df-mnf 9928  df-xr 9929  df-ltxr 9930  df-le 9931  df-sub 10114  df-neg 10115  df-div 10529  df-nn 10863  df-2 10921  df-3 10922  df-4 10923  df-5 10924  df-6 10925  df-7 10926  df-8 10927  df-9 10928  df-n0 11135  df-z 11206  df-dec 11321  df-uz 11515  df-q 11616  df-rp 11660  df-xneg 11773  df-xadd 11774  df-xmul 11775  df-ioo 12001  df-ico 12003  df-icc 12004  df-fz 12148  df-fzo 12285  df-fl 12405  df-seq 12614  df-exp 12673  df-hash 12930  df-cj 13628  df-re 13629  df-im 13630  df-sqrt 13764  df-abs 13765  df-clim 14008  df-rlim 14009  df-sum 14206  df-prod 14416  df-struct 15638  df-ndx 15639  df-slot 15640  df-base 15641  df-sets 15642  df-ress 15643  df-plusg 15722  df-mulr 15723  df-starv 15724  df-sca 15725  df-vsca 15726  df-ip 15727  df-tset 15728  df-ple 15729  df-ds 15732  df-unif 15733  df-hom 15734  df-cco 15735  df-rest 15847  df-topn 15848  df-0g 15866  df-gsum 15867  df-topgen 15868  df-prds 15872  df-pws 15874  df-mgm 17006  df-sgrp 17048  df-mnd 17059  df-mhm 17099  df-submnd 17100  df-grp 17189  df-minusg 17190  df-sbg 17191  df-subg 17355  df-ghm 17422  df-cntz 17514  df-cmn 17959  df-abl 17960  df-mgp 18254  df-ur 18266  df-ring 18313  df-cring 18314  df-oppr 18387  df-dvdsr 18405  df-unit 18406  df-invr 18436  df-dvr 18447  df-rnghom 18479  df-drng 18513  df-field 18514  df-subrg 18542  df-abv 18581  df-staf 18609  df-srng 18610  df-lmod 18629  df-lss 18695  df-lmhm 18784  df-lvec 18865  df-sra 18934  df-rgmod 18935  df-psmet 19500  df-xmet 19501  df-met 19502  df-bl 19503  df-mopn 19504  df-cnfld 19509  df-refld 19710  df-phl 19730  df-dsmm 19832  df-frlm 19847  df-top 20458  df-bases 20459  df-topon 20460  df-topsp 20461  df-cmp 20937  df-xms 21871  df-ms 21872  df-nm 22133  df-ngp 22134  df-tng 22135  df-nrg 22136  df-nlm 22137  df-clm 22597  df-cph 22695  df-tch 22696  df-rrx 22893  df-ovol 22952  df-vol 22953  df-salg 39004  df-sumge0 39055  df-mea 39142  df-ome 39179  df-caragen 39181  df-ovoln 39226  df-voln 39228
This theorem is referenced by:  opnvonmbl  39323
  Copyright terms: Public domain W3C validator