Step | Hyp | Ref
| Expression |
1 | | opnvonmbllem2.x |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ Fin) |
2 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(dist‘(ℝ^‘𝑋)) = (dist‘(ℝ^‘𝑋)) |
3 | 2 | rrxmetfi 40507 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Fin →
(dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
4 | 1, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ
↑𝑚 𝑋))) |
5 | | metxmet 22139 |
. . . . . . . . . 10
⊢
((dist‘(ℝ^‘𝑋)) ∈ (Met‘(ℝ
↑𝑚 𝑋)) → (dist‘(ℝ^‘𝑋)) ∈
(∞Met‘(ℝ ↑𝑚 𝑋))) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ
↑𝑚 𝑋))) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (dist‘(ℝ^‘𝑋)) ∈
(∞Met‘(ℝ ↑𝑚 𝑋))) |
8 | | opnvonmbllem2.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) |
9 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(ℝ^‘𝑋) =
(ℝ^‘𝑋) |
10 | 9 | rrxval 23175 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin →
(ℝ^‘𝑋) =
(toℂHil‘(ℝfld freeLMod 𝑋))) |
11 | 1, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (ℝ^‘𝑋) =
(toℂHil‘(ℝfld freeLMod 𝑋))) |
12 | 11 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) =
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋)))) |
13 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢
(ℝfld freeLMod 𝑋) ∈ V |
14 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(toℂHil‘(ℝfld freeLMod 𝑋)) =
(toℂHil‘(ℝfld freeLMod 𝑋)) |
15 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(dist‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(dist‘(toℂHil‘(ℝfld freeLMod 𝑋))) |
16 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) |
17 | 14, 15, 16 | tchtopn 23025 |
. . . . . . . . . . . . 13
⊢
((ℝfld freeLMod 𝑋) ∈ V →
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod
𝑋))))) |
18 | 13, 17 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod
𝑋)))) |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 →
(TopOpen‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod
𝑋))))) |
20 | 11 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(toℂHil‘(ℝfld freeLMod 𝑋)) = (ℝ^‘𝑋)) |
21 | 20 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(dist‘(toℂHil‘(ℝfld freeLMod 𝑋))) =
(dist‘(ℝ^‘𝑋))) |
22 | 21 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝜑 →
(MetOpen‘(dist‘(toℂHil‘(ℝfld freeLMod
𝑋)))) =
(MetOpen‘(dist‘(ℝ^‘𝑋)))) |
23 | 12, 19, 22 | 3eqtrd 2660 |
. . . . . . . . . 10
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) =
(MetOpen‘(dist‘(ℝ^‘𝑋)))) |
24 | 8, 23 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈
(MetOpen‘(dist‘(ℝ^‘𝑋)))) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ∈
(MetOpen‘(dist‘(ℝ^‘𝑋)))) |
26 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺) |
27 | | eqid 2622 |
. . . . . . . . 9
⊢
(MetOpen‘(dist‘(ℝ^‘𝑋))) =
(MetOpen‘(dist‘(ℝ^‘𝑋))) |
28 | 27 | mopni2 22298 |
. . . . . . . 8
⊢
(((dist‘(ℝ^‘𝑋)) ∈ (∞Met‘(ℝ
↑𝑚 𝑋)) ∧ 𝐺 ∈
(MetOpen‘(dist‘(ℝ^‘𝑋))) ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) |
29 | 7, 25, 26, 28 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) |
30 | 1 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑋 ∈ Fin) |
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(TopOpen‘(ℝ^‘𝑋)) = (TopOpen‘(ℝ^‘𝑋)) |
32 | 31 | rrxtoponfi 40511 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ Fin →
(TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ
↑𝑚 𝑋))) |
33 | 1, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ
↑𝑚 𝑋))) |
34 | | toponss 20731 |
. . . . . . . . . . . . . . . 16
⊢
(((TopOpen‘(ℝ^‘𝑋)) ∈ (TopOn‘(ℝ
↑𝑚 𝑋)) ∧ 𝐺 ∈ (TopOpen‘(ℝ^‘𝑋))) → 𝐺 ⊆ (ℝ ↑𝑚
𝑋)) |
35 | 33, 8, 34 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺 ⊆ (ℝ ↑𝑚
𝑋)) |
36 | 35 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐺 ⊆ (ℝ ↑𝑚
𝑋)) |
37 | 36, 26 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ (ℝ ↑𝑚
𝑋)) |
38 | 37 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑥 ∈ (ℝ
↑𝑚 𝑋)) |
39 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
40 | 30, 38, 39 | hoiqssbl 40839 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+) →
∃𝑐 ∈ (ℚ
↑𝑚 𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) |
41 | 40 | 3adant3 1081 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) |
42 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖(𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) |
43 | | nfv 1843 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖(𝑐 ∈ (ℚ
↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) |
44 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖𝑥 |
45 | | nfixp1 7928 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) |
46 | 44, 45 | nfel 2777 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖 𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) |
47 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑖(𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) |
48 | 45, 47 | nfss 3596 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑖X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) |
49 | 46, 48 | nfan 1828 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑖(𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) |
50 | 42, 43, 49 | nf3an 1831 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑖((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) |
51 | 1 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → 𝑋 ∈ Fin) |
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑋 ∈ Fin) |
53 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ (ℚ
↑𝑚 𝑋) → 𝑐:𝑋⟶ℚ) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ (ℚ
↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) → 𝑐:𝑋⟶ℚ) |
55 | 54 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑐:𝑋⟶ℚ) |
56 | | elmapi 7879 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 ∈ (ℚ
↑𝑚 𝑋) → 𝑑:𝑋⟶ℚ) |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ (ℚ
↑𝑚 𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) → 𝑑:𝑋⟶ℚ) |
58 | 57 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑑:𝑋⟶ℚ) |
59 | | simp3r 1090 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) |
60 | | simp1r 1086 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) |
61 | | simp3l 1089 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → 𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖))) |
62 | | opnvonmbl.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 = {ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} |
63 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ 𝑋 ↦ 〈(𝑐‘𝑖), (𝑑‘𝑖)〉) = (𝑖 ∈ 𝑋 ↦ 〈(𝑐‘𝑖), (𝑑‘𝑖)〉) |
64 | 50, 52, 55, 58, 59, 60, 61, 62, 63 | opnvonmbllem1 40846 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) ∧ (𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) ∧ (𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒))) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
65 | 64 | 3exp 1264 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) → ((𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))) |
66 | 65 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) → ((𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))) |
67 | 66 | 3adant2 1080 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ((𝑐 ∈ (ℚ ↑𝑚
𝑋) ∧ 𝑑 ∈ (ℚ ↑𝑚
𝑋)) → ((𝑥 ∈ X𝑖 ∈
𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))) |
68 | 67 | rexlimdvv 3037 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → (∃𝑐 ∈ (ℚ ↑𝑚
𝑋)∃𝑑 ∈ (ℚ ↑𝑚
𝑋)(𝑥 ∈ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ∧ X𝑖 ∈ 𝑋 ((𝑐‘𝑖)[,)(𝑑‘𝑖)) ⊆ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒)) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))) |
69 | 41, 68 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑒 ∈ ℝ+ ∧ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
70 | 69 | 3exp 1264 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝑒 ∈ ℝ+ → ((𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)))) |
71 | 70 | rexlimdv 3030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑒 ∈ ℝ+ (𝑥(ball‘(dist‘(ℝ^‘𝑋)))𝑒) ⊆ 𝐺 → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖))) |
72 | 29, 71 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
73 | | eliun 4524 |
. . . . . 6
⊢ (𝑥 ∈ ∪ ℎ
∈ 𝐾 X𝑖 ∈
𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∃ℎ ∈ 𝐾 𝑥 ∈ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
74 | 72, 73 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ∪
ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
75 | 74 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪
ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
76 | | dfss3 3592 |
. . . 4
⊢ (𝐺 ⊆ ∪ ℎ
∈ 𝐾 X𝑖 ∈
𝑋 (([,) ∘ ℎ)‘𝑖) ↔ ∀𝑥 ∈ 𝐺 𝑥 ∈ ∪
ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
77 | 75, 76 | sylibr 224 |
. . 3
⊢ (𝜑 → 𝐺 ⊆ ∪
ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
78 | 62 | eleq2i 2693 |
. . . . . . . . 9
⊢ (ℎ ∈ 𝐾 ↔ ℎ ∈ {ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}) |
79 | 78 | biimpi 206 |
. . . . . . . 8
⊢ (ℎ ∈ 𝐾 → ℎ ∈ {ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}) |
80 | 79 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ ∈ {ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺}) |
81 | | rabid 3116 |
. . . . . . 7
⊢ (ℎ ∈ {ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ↔ (ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)) |
82 | 80, 81 | sylib 208 |
. . . . . 6
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋) ∧ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺)) |
83 | 82 | simprd 479 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺) |
84 | 83 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺) |
85 | | iunss 4561 |
. . . 4
⊢ (∪ ℎ
∈ 𝐾 X𝑖 ∈
𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺 ↔ ∀ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺) |
86 | 84, 85 | sylibr 224 |
. . 3
⊢ (𝜑 → ∪ ℎ
∈ 𝐾 X𝑖 ∈
𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺) |
87 | 77, 86 | eqssd 3620 |
. 2
⊢ (𝜑 → 𝐺 = ∪ ℎ ∈ 𝐾 X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖)) |
88 | | opnvonmbllem2.n |
. . . 4
⊢ 𝑆 = dom (voln‘𝑋) |
89 | 1, 88 | dmovnsal 40826 |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
90 | | ssrab2 3687 |
. . . . . 6
⊢ {ℎ ∈ ((ℚ ×
ℚ) ↑𝑚 𝑋) ∣ X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ⊆ 𝐺} ⊆ ((ℚ × ℚ)
↑𝑚 𝑋) |
91 | 62, 90 | eqsstri 3635 |
. . . . 5
⊢ 𝐾 ⊆ ((ℚ ×
ℚ) ↑𝑚 𝑋) |
92 | 91 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐾 ⊆ ((ℚ × ℚ)
↑𝑚 𝑋)) |
93 | | qct 39578 |
. . . . . . 7
⊢ ℚ
≼ ω |
94 | 93 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℚ ≼
ω) |
95 | | xpct 8839 |
. . . . . 6
⊢ ((ℚ
≼ ω ∧ ℚ ≼ ω) → (ℚ × ℚ)
≼ ω) |
96 | 94, 94, 95 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (ℚ × ℚ)
≼ ω) |
97 | 96, 1 | mpct 39393 |
. . . 4
⊢ (𝜑 → ((ℚ × ℚ)
↑𝑚 𝑋) ≼ ω) |
98 | | ssct 8041 |
. . . 4
⊢ ((𝐾 ⊆ ((ℚ ×
ℚ) ↑𝑚 𝑋) ∧ ((ℚ × ℚ)
↑𝑚 𝑋) ≼ ω) → 𝐾 ≼ ω) |
99 | 92, 97, 98 | syl2anc 693 |
. . 3
⊢ (𝜑 → 𝐾 ≼ ω) |
100 | | reex 10027 |
. . . . . . . . . 10
⊢ ℝ
∈ V |
101 | 100, 100 | xpex 6962 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ∈ V |
102 | | qssre 11798 |
. . . . . . . . . 10
⊢ ℚ
⊆ ℝ |
103 | | xpss12 5225 |
. . . . . . . . . 10
⊢ ((ℚ
⊆ ℝ ∧ ℚ ⊆ ℝ) → (ℚ × ℚ)
⊆ (ℝ × ℝ)) |
104 | 102, 102,
103 | mp2an 708 |
. . . . . . . . 9
⊢ (ℚ
× ℚ) ⊆ (ℝ × ℝ) |
105 | | mapss 7900 |
. . . . . . . . 9
⊢
(((ℝ × ℝ) ∈ V ∧ (ℚ × ℚ)
⊆ (ℝ × ℝ)) → ((ℚ × ℚ)
↑𝑚 𝑋) ⊆ ((ℝ × ℝ)
↑𝑚 𝑋)) |
106 | 101, 104,
105 | mp2an 708 |
. . . . . . . 8
⊢ ((ℚ
× ℚ) ↑𝑚 𝑋) ⊆ ((ℝ × ℝ)
↑𝑚 𝑋) |
107 | 91 | sseli 3599 |
. . . . . . . 8
⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℚ × ℚ)
↑𝑚 𝑋)) |
108 | 106, 107 | sseldi 3601 |
. . . . . . 7
⊢ (ℎ ∈ 𝐾 → ℎ ∈ ((ℝ × ℝ)
↑𝑚 𝑋)) |
109 | | elmapi 7879 |
. . . . . . 7
⊢ (ℎ ∈ ((ℝ ×
ℝ) ↑𝑚 𝑋) → ℎ:𝑋⟶(ℝ ×
ℝ)) |
110 | 108, 109 | syl 17 |
. . . . . 6
⊢ (ℎ ∈ 𝐾 → ℎ:𝑋⟶(ℝ ×
ℝ)) |
111 | 110 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → ℎ:𝑋⟶(ℝ ×
ℝ)) |
112 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (ℎ‘𝑘) = (ℎ‘𝑖)) |
113 | 112 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (1st ‘(ℎ‘𝑘)) = (1st ‘(ℎ‘𝑖))) |
114 | 113 | cbvmptv 4750 |
. . . . 5
⊢ (𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑖))) |
115 | 112 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 𝑖 → (2nd ‘(ℎ‘𝑘)) = (2nd ‘(ℎ‘𝑖))) |
116 | 115 | cbvmptv 4750 |
. . . . 5
⊢ (𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘))) = (𝑖 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑖))) |
117 | 111, 114,
116 | hoicoto2 40819 |
. . . 4
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) = X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘)))‘𝑖))) |
118 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → 𝑋 ∈ Fin) |
119 | 111 | ffvelrnda 6359 |
. . . . . . 7
⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (ℎ‘𝑘) ∈ (ℝ ×
ℝ)) |
120 | | xp1st 7198 |
. . . . . . 7
⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) →
(1st ‘(ℎ‘𝑘)) ∈ ℝ) |
121 | 119, 120 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (1st ‘(ℎ‘𝑘)) ∈ ℝ) |
122 | | eqid 2622 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘))) = (𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘))) |
123 | 121, 122 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘))):𝑋⟶ℝ) |
124 | | xp2nd 7199 |
. . . . . . 7
⊢ ((ℎ‘𝑘) ∈ (ℝ × ℝ) →
(2nd ‘(ℎ‘𝑘)) ∈ ℝ) |
125 | 119, 124 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ ℎ ∈ 𝐾) ∧ 𝑘 ∈ 𝑋) → (2nd ‘(ℎ‘𝑘)) ∈ ℝ) |
126 | | eqid 2622 |
. . . . . 6
⊢ (𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘))) = (𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘))) |
127 | 125, 126 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → (𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘))):𝑋⟶ℝ) |
128 | 118, 88, 123, 127 | hoimbl 40845 |
. . . 4
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (((𝑘 ∈ 𝑋 ↦ (1st ‘(ℎ‘𝑘)))‘𝑖)[,)((𝑘 ∈ 𝑋 ↦ (2nd ‘(ℎ‘𝑘)))‘𝑖)) ∈ 𝑆) |
129 | 117, 128 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ ℎ ∈ 𝐾) → X𝑖 ∈ 𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆) |
130 | 89, 99, 129 | saliuncl 40542 |
. 2
⊢ (𝜑 → ∪ ℎ
∈ 𝐾 X𝑖 ∈
𝑋 (([,) ∘ ℎ)‘𝑖) ∈ 𝑆) |
131 | 87, 130 | eqeltrd 2701 |
1
⊢ (𝜑 → 𝐺 ∈ 𝑆) |