Step |
Hyp |
Ref |
Expression |
1 |
|
prdsxms.y |
⊢ 𝑌 = ( 𝑆 Xs 𝑅 ) |
2 |
|
prdsxms.s |
⊢ ( 𝜑 → 𝑆 ∈ 𝑊 ) |
3 |
|
prdsxms.i |
⊢ ( 𝜑 → 𝐼 ∈ Fin ) |
4 |
|
prdsxms.d |
⊢ 𝐷 = ( dist ‘ 𝑌 ) |
5 |
|
prdsxms.b |
⊢ 𝐵 = ( Base ‘ 𝑌 ) |
6 |
|
prdsxms.r |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ ∞MetSp ) |
7 |
|
prdsxms.j |
⊢ 𝐽 = ( TopOpen ‘ 𝑌 ) |
8 |
|
prdsxms.v |
⊢ 𝑉 = ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) |
9 |
|
prdsxms.e |
⊢ 𝐸 = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( 𝑉 × 𝑉 ) ) |
10 |
|
prdsxms.k |
⊢ 𝐾 = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) |
11 |
|
prdsxms.c |
⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) } |
12 |
|
topnfn |
⊢ TopOpen Fn V |
13 |
6
|
ffnd |
⊢ ( 𝜑 → 𝑅 Fn 𝐼 ) |
14 |
|
dffn2 |
⊢ ( 𝑅 Fn 𝐼 ↔ 𝑅 : 𝐼 ⟶ V ) |
15 |
13 14
|
sylib |
⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ V ) |
16 |
|
fnfco |
⊢ ( ( TopOpen Fn V ∧ 𝑅 : 𝐼 ⟶ V ) → ( TopOpen ∘ 𝑅 ) Fn 𝐼 ) |
17 |
12 15 16
|
sylancr |
⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) Fn 𝐼 ) |
18 |
11
|
ptval |
⊢ ( ( 𝐼 ∈ Fin ∧ ( TopOpen ∘ 𝑅 ) Fn 𝐼 ) → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ 𝐶 ) ) |
19 |
3 17 18
|
syl2anc |
⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ 𝐶 ) ) |
20 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ↔ ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑥 ≠ ∅ ) ) |
21 |
1 2 3 4 5 6
|
prdsxmslem1 |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ) |
22 |
|
blrn |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) ) |
23 |
21 22
|
syl |
⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ↔ ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) ) |
24 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ) |
25 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → 𝑝 ∈ 𝐵 ) |
26 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → 𝑟 ∈ ℝ* ) |
27 |
|
xbln0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) ) |
28 |
24 25 26 27
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ↔ 0 < 𝑟 ) ) |
29 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐼 ∈ Fin ) |
30 |
29
|
mptexd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∈ V ) |
31 |
|
ovex |
⊢ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V |
32 |
31
|
rgenw |
⊢ ∀ 𝑛 ∈ 𝐼 ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V |
33 |
|
eqid |
⊢ ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) |
34 |
33
|
fnmpt |
⊢ ( ∀ 𝑛 ∈ 𝐼 ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ∈ V → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ) |
35 |
32 34
|
mp1i |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ) |
36 |
6
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑅 : 𝐼 ⟶ ∞MetSp ) |
37 |
36
|
ffvelrnda |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp ) |
38 |
8 9
|
xmsxmet |
⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ) |
39 |
37 38
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ) |
40 |
|
eqid |
⊢ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) |
41 |
|
eqid |
⊢ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) |
42 |
2
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑆 ∈ 𝑊 ) |
43 |
37
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp ) |
44 |
|
simp2l |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ 𝐵 ) |
45 |
36
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑅 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) |
46 |
45
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) |
47 |
1 46
|
syl5eq |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) |
48 |
47
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) |
49 |
5 48
|
syl5eq |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) |
50 |
44 49
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) |
51 |
40 41 42 29 43 8 50
|
prdsbascl |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 ) |
52 |
51
|
r19.21bi |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 ) |
53 |
|
simp2r |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑟 ∈ ℝ* ) |
54 |
53
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝑟 ∈ ℝ* ) |
55 |
|
eqid |
⊢ ( MetOpen ‘ 𝐸 ) = ( MetOpen ‘ 𝐸 ) |
56 |
55
|
blopn |
⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑉 ∧ 𝑟 ∈ ℝ* ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐸 ) ) |
57 |
39 52 54 56
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐸 ) ) |
58 |
|
2fveq3 |
⊢ ( 𝑛 = 𝑘 → ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) = ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
59 |
|
2fveq3 |
⊢ ( 𝑛 = 𝑘 → ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
60 |
59 8
|
eqtr4di |
⊢ ( 𝑛 = 𝑘 → ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) = 𝑉 ) |
61 |
60
|
sqxpeqd |
⊢ ( 𝑛 = 𝑘 → ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) = ( 𝑉 × 𝑉 ) ) |
62 |
58 61
|
reseq12d |
⊢ ( 𝑛 = 𝑘 → ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( 𝑉 × 𝑉 ) ) ) |
63 |
62 9
|
eqtr4di |
⊢ ( 𝑛 = 𝑘 → ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) = 𝐸 ) |
64 |
63
|
fveq2d |
⊢ ( 𝑛 = 𝑘 → ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) = ( ball ‘ 𝐸 ) ) |
65 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑝 ‘ 𝑛 ) = ( 𝑝 ‘ 𝑘 ) ) |
66 |
|
eqidd |
⊢ ( 𝑛 = 𝑘 → 𝑟 = 𝑟 ) |
67 |
64 65 66
|
oveq123d |
⊢ ( 𝑛 = 𝑘 → ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
68 |
|
ovex |
⊢ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ∈ V |
69 |
67 33 68
|
fvmpt |
⊢ ( 𝑘 ∈ 𝐼 → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
70 |
69
|
adantl |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
71 |
|
fvco3 |
⊢ ( ( 𝑅 : 𝐼 ⟶ ∞MetSp ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( TopOpen ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
72 |
71 10
|
eqtr4di |
⊢ ( ( 𝑅 : 𝐼 ⟶ ∞MetSp ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 ) |
73 |
36 72
|
sylan |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 ) |
74 |
10 8 9
|
xmstopn |
⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → 𝐾 = ( MetOpen ‘ 𝐸 ) ) |
75 |
37 74
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → 𝐾 = ( MetOpen ‘ 𝐸 ) ) |
76 |
73 75
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( MetOpen ‘ 𝐸 ) ) |
77 |
57 70 76
|
3eltr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
78 |
77
|
ralrimiva |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
79 |
36
|
feqmptd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑅 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) |
80 |
79
|
oveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) |
81 |
1 80
|
syl5eq |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑌 = ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) |
82 |
81
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) |
83 |
4 82
|
syl5eq |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) |
84 |
83
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( ball ‘ 𝐷 ) = ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) ) |
85 |
84
|
oveqd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) |
86 |
|
fveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑅 ‘ 𝑛 ) = ( 𝑅 ‘ 𝑘 ) ) |
87 |
86
|
cbvmptv |
⊢ ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) |
88 |
87
|
oveq2i |
⊢ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) |
89 |
|
eqid |
⊢ ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) |
90 |
|
eqid |
⊢ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) |
91 |
81
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) |
92 |
5 91
|
syl5eq |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) |
93 |
44 92
|
eleqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 𝑝 ∈ ( Base ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) |
94 |
|
simp3 |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → 0 < 𝑟 ) |
95 |
88 89 8 9 90 42 29 37 39 93 53 94
|
prdsbl |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ ( dist ‘ ( 𝑆 Xs ( 𝑛 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
96 |
85 95
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
97 |
|
fneq1 |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( 𝑔 Fn 𝐼 ↔ ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ) ) |
98 |
|
fveq1 |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ) |
99 |
98
|
eleq1d |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) |
100 |
99
|
ralbidv |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) |
101 |
97 100
|
anbi12d |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) ) |
102 |
98 69
|
sylan9eq |
⊢ ( ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑘 ) = ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
103 |
102
|
ixpeq2dva |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
104 |
103
|
eqeq2d |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) |
105 |
101 104
|
anbi12d |
⊢ ( 𝑔 = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) ) |
106 |
105
|
spcegv |
⊢ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∈ V → ( ( ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
107 |
106
|
3impib |
⊢ ( ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ∈ V ∧ ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑝 ‘ 𝑛 ) ( ball ‘ ( ( dist ‘ ( 𝑅 ‘ 𝑛 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑛 ) ) ) ) ) 𝑟 ) ) ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) |
108 |
30 35 78 96 107
|
syl121anc |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ∧ 0 < 𝑟 ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) |
109 |
108
|
3expia |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( 0 < 𝑟 → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
110 |
28 109
|
sylbid |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
111 |
110
|
adantr |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
112 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) |
113 |
112
|
neeq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑥 ≠ ∅ ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ≠ ∅ ) ) |
114 |
|
df-3an |
⊢ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) |
115 |
|
ral0 |
⊢ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) |
116 |
|
difeq2 |
⊢ ( 𝑧 = 𝐼 → ( 𝐼 ∖ 𝑧 ) = ( 𝐼 ∖ 𝐼 ) ) |
117 |
|
difid |
⊢ ( 𝐼 ∖ 𝐼 ) = ∅ |
118 |
116 117
|
eqtrdi |
⊢ ( 𝑧 = 𝐼 → ( 𝐼 ∖ 𝑧 ) = ∅ ) |
119 |
118
|
raleqdv |
⊢ ( 𝑧 = 𝐼 → ( ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) |
120 |
119
|
rspcev |
⊢ ( ( 𝐼 ∈ Fin ∧ ∀ 𝑘 ∈ ∅ ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
121 |
3 115 120
|
sylancl |
⊢ ( 𝜑 → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
122 |
121
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
123 |
122
|
biantrud |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) ) |
124 |
114 123
|
bitr4id |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ↔ ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ) ) |
125 |
|
eqeq1 |
⊢ ( 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) |
126 |
124 125
|
bi2anan9 |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
127 |
126
|
exbidv |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
128 |
111 113 127
|
3imtr4d |
⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) ∧ 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
129 |
128
|
ex |
⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) ) → ( 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) ) |
130 |
129
|
rexlimdvva |
⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐵 ∃ 𝑟 ∈ ℝ* 𝑥 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) ) |
131 |
23 130
|
sylbid |
⊢ ( 𝜑 → ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) → ( 𝑥 ≠ ∅ → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) ) |
132 |
131
|
impd |
⊢ ( 𝜑 → ( ( 𝑥 ∈ ran ( ball ‘ 𝐷 ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
133 |
20 132
|
syl5bi |
⊢ ( 𝜑 → ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
134 |
133
|
alrimiv |
⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
135 |
|
ssab |
⊢ ( ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) } ↔ ∀ 𝑥 ( 𝑥 ∈ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) → ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) ) ) |
136 |
134 135
|
sylibr |
⊢ ( 𝜑 → ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑧 ) ( 𝑔 ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) ∧ 𝑥 = X 𝑘 ∈ 𝐼 ( 𝑔 ‘ 𝑘 ) ) } ) |
137 |
136 11
|
sseqtrrdi |
⊢ ( 𝜑 → ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ 𝐶 ) |
138 |
|
ssv |
⊢ ∞MetSp ⊆ V |
139 |
|
fnssres |
⊢ ( ( TopOpen Fn V ∧ ∞MetSp ⊆ V ) → ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp ) |
140 |
12 138 139
|
mp2an |
⊢ ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp |
141 |
|
fvres |
⊢ ( 𝑥 ∈ ∞MetSp → ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 ) ) |
142 |
|
xmstps |
⊢ ( 𝑥 ∈ ∞MetSp → 𝑥 ∈ TopSp ) |
143 |
|
eqid |
⊢ ( TopOpen ‘ 𝑥 ) = ( TopOpen ‘ 𝑥 ) |
144 |
143
|
tpstop |
⊢ ( 𝑥 ∈ TopSp → ( TopOpen ‘ 𝑥 ) ∈ Top ) |
145 |
142 144
|
syl |
⊢ ( 𝑥 ∈ ∞MetSp → ( TopOpen ‘ 𝑥 ) ∈ Top ) |
146 |
141 145
|
eqeltrd |
⊢ ( 𝑥 ∈ ∞MetSp → ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top ) |
147 |
146
|
rgen |
⊢ ∀ 𝑥 ∈ ∞MetSp ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top |
148 |
|
ffnfv |
⊢ ( ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top ↔ ( ( TopOpen ↾ ∞MetSp ) Fn ∞MetSp ∧ ∀ 𝑥 ∈ ∞MetSp ( ( TopOpen ↾ ∞MetSp ) ‘ 𝑥 ) ∈ Top ) ) |
149 |
140 147 148
|
mpbir2an |
⊢ ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top |
150 |
|
fco2 |
⊢ ( ( ( TopOpen ↾ ∞MetSp ) : ∞MetSp ⟶ Top ∧ 𝑅 : 𝐼 ⟶ ∞MetSp ) → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ) |
151 |
149 6 150
|
sylancr |
⊢ ( 𝜑 → ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ) |
152 |
|
eqid |
⊢ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) |
153 |
11 152
|
ptbasfi |
⊢ ( ( 𝐼 ∈ Fin ∧ ( TopOpen ∘ 𝑅 ) : 𝐼 ⟶ Top ) → 𝐶 = ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ) |
154 |
3 151 153
|
syl2anc |
⊢ ( 𝜑 → 𝐶 = ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ) |
155 |
|
eqid |
⊢ ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ 𝐷 ) |
156 |
155
|
mopntop |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) ∈ Top ) |
157 |
21 156
|
syl |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ∈ Top ) |
158 |
1 5 2 3 13
|
prdsbas2 |
⊢ ( 𝜑 → 𝐵 = X 𝑘 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) |
159 |
6 72
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = 𝐾 ) |
160 |
6
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp ) |
161 |
|
xmstps |
⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ ∞MetSp → ( 𝑅 ‘ 𝑘 ) ∈ TopSp ) |
162 |
160 161
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ TopSp ) |
163 |
8 10
|
istps |
⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ 𝑉 ) ) |
164 |
162 163
|
sylib |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐾 ∈ ( TopOn ‘ 𝑉 ) ) |
165 |
159 164
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∈ ( TopOn ‘ 𝑉 ) ) |
166 |
|
toponuni |
⊢ ( ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ∈ ( TopOn ‘ 𝑉 ) → 𝑉 = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
167 |
165 166
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑉 = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
168 |
8 167
|
eqtr3id |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
169 |
168
|
ixpeq2dva |
⊢ ( 𝜑 → X 𝑘 ∈ 𝐼 ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
170 |
158 169
|
eqtrd |
⊢ ( 𝜑 → 𝐵 = X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ) |
171 |
|
fveq2 |
⊢ ( 𝑘 = 𝑛 → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ) |
172 |
171
|
unieqd |
⊢ ( 𝑘 = 𝑛 → ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ) |
173 |
172
|
cbvixpv |
⊢ X 𝑘 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) |
174 |
170 173
|
eqtrdi |
⊢ ( 𝜑 → 𝐵 = X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ) |
175 |
155
|
mopntopon |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) ) |
176 |
21 175
|
syl |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) ) |
177 |
|
toponmax |
⊢ ( ( MetOpen ‘ 𝐷 ) ∈ ( TopOn ‘ 𝐵 ) → 𝐵 ∈ ( MetOpen ‘ 𝐷 ) ) |
178 |
176 177
|
syl |
⊢ ( 𝜑 → 𝐵 ∈ ( MetOpen ‘ 𝐷 ) ) |
179 |
174 178
|
eqeltrrd |
⊢ ( 𝜑 → X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
180 |
179
|
snssd |
⊢ ( 𝜑 → { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ⊆ ( MetOpen ‘ 𝐷 ) ) |
181 |
174
|
mpteq1d |
⊢ ( 𝜑 → ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
182 |
181
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
183 |
182
|
cnveqd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) ) |
184 |
183
|
imaeq1d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
185 |
|
fveq1 |
⊢ ( 𝑤 = 𝑝 → ( 𝑤 ‘ 𝑘 ) = ( 𝑝 ‘ 𝑘 ) ) |
186 |
185
|
eleq1d |
⊢ ( 𝑤 = 𝑝 → ( ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) |
187 |
|
eqid |
⊢ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) |
188 |
187
|
mptpreima |
⊢ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑤 ∈ 𝐵 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 } |
189 |
186 188
|
elrab2 |
⊢ ( 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) |
190 |
160 38
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ) |
191 |
190
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ) |
192 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑢 ∈ 𝐾 ) |
193 |
160 74
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐾 = ( MetOpen ‘ 𝐸 ) ) |
194 |
193
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝐾 = ( MetOpen ‘ 𝐸 ) ) |
195 |
192 194
|
eleqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑢 ∈ ( MetOpen ‘ 𝐸 ) ) |
196 |
|
simprrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) |
197 |
55
|
mopni2 |
⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ 𝑢 ∈ ( MetOpen ‘ 𝐸 ) ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑟 ∈ ℝ+ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) |
198 |
191 195 196 197
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ∃ 𝑟 ∈ ℝ+ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) |
199 |
21
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ) |
200 |
|
simprrl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → 𝑝 ∈ 𝐵 ) |
201 |
200
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑝 ∈ 𝐵 ) |
202 |
|
rpxr |
⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* ) |
203 |
202
|
ad2antrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ* ) |
204 |
155
|
blopn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
205 |
199 201 203 204
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
206 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑟 ∈ ℝ+ ) |
207 |
|
blcntr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ+ ) → 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) |
208 |
199 201 206 207
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) |
209 |
|
blssm |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ∧ 𝑟 ∈ ℝ* ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 ) |
210 |
199 201 203 209
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝐵 ) |
211 |
|
simplrr |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) |
212 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 𝜑 ) |
213 |
|
rpgt0 |
⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 ) |
214 |
213
|
ad2antrl |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → 0 < 𝑟 ) |
215 |
212 201 203 214 96
|
syl121anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) = X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
216 |
215
|
eleq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ↔ 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) |
217 |
216
|
biimpa |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
218 |
|
vex |
⊢ 𝑤 ∈ V |
219 |
218
|
elixp |
⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ↔ ( 𝑤 Fn 𝐼 ∧ ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) |
220 |
219
|
simprbi |
⊢ ( 𝑤 ∈ X 𝑘 ∈ 𝐼 ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) → ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
221 |
217 220
|
syl |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
222 |
|
simp-4r |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → 𝑘 ∈ 𝐼 ) |
223 |
|
rsp |
⊢ ( ∀ 𝑘 ∈ 𝐼 ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) → ( 𝑘 ∈ 𝐼 → ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) ) |
224 |
221 222 223
|
sylc |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ) |
225 |
211 224
|
sseldd |
⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) ∧ 𝑤 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 ) |
226 |
210 225
|
ssrabdv |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ { 𝑤 ∈ 𝐵 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 } ) |
227 |
226 188
|
sseqtrrdi |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) |
228 |
|
eleq2 |
⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑝 ∈ 𝑦 ↔ 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ) ) |
229 |
|
sseq1 |
⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) |
230 |
228 229
|
anbi12d |
⊢ ( 𝑦 = ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ↔ ( 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) |
231 |
230
|
rspcev |
⊢ ( ( ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∈ ( MetOpen ‘ 𝐷 ) ∧ ( 𝑝 ∈ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑝 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) |
232 |
205 208 227 231
|
syl12anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑝 ‘ 𝑘 ) ( ball ‘ 𝐸 ) 𝑟 ) ⊆ 𝑢 ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) |
233 |
198 232
|
rexlimddv |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ ( 𝑢 ∈ 𝐾 ∧ ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) |
234 |
233
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑝 ∈ 𝐵 ∧ ( 𝑝 ‘ 𝑘 ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) |
235 |
189 234
|
syl5bi |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) |
236 |
235
|
ralrimiv |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ∀ 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) |
237 |
157
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( MetOpen ‘ 𝐷 ) ∈ Top ) |
238 |
|
eltop2 |
⊢ ( ( MetOpen ‘ 𝐷 ) ∈ Top → ( ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) |
239 |
237 238
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑝 ∈ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∃ 𝑦 ∈ ( MetOpen ‘ 𝐷 ) ( 𝑝 ∈ 𝑦 ∧ 𝑦 ⊆ ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) ) |
240 |
236 239
|
mpbird |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( 𝑤 ∈ 𝐵 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
241 |
184 240
|
eqeltrrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑢 ∈ 𝐾 ) → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
242 |
241
|
ralrimiva |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑢 ∈ 𝐾 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
243 |
159
|
raleqdv |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑢 ∈ 𝐾 ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) ) |
244 |
242 243
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
245 |
244
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
246 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) = ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) |
247 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑚 ) ) |
248 |
247
|
mpteq2dv |
⊢ ( 𝑘 = 𝑚 → ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) ) |
249 |
248
|
cnveqd |
⊢ ( 𝑘 = 𝑚 → ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) = ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) ) |
250 |
249
|
imaeq1d |
⊢ ( 𝑘 = 𝑚 → ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) |
251 |
250
|
eleq1d |
⊢ ( 𝑘 = 𝑚 → ( ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) ) |
252 |
246 251
|
raleqbidv |
⊢ ( 𝑘 = 𝑚 → ( ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) ) |
253 |
252
|
cbvralvw |
⊢ ( ∀ 𝑘 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑘 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
254 |
245 253
|
sylib |
⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ) |
255 |
|
eqid |
⊢ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) = ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) |
256 |
255
|
fmpox |
⊢ ( ∀ 𝑚 ∈ 𝐼 ∀ 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ∈ ( MetOpen ‘ 𝐷 ) ↔ ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) ) |
257 |
254 256
|
sylib |
⊢ ( 𝜑 → ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) : ∪ 𝑚 ∈ 𝐼 ( { 𝑚 } × ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ) ⟶ ( MetOpen ‘ 𝐷 ) ) |
258 |
257
|
frnd |
⊢ ( 𝜑 → ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ⊆ ( MetOpen ‘ 𝐷 ) ) |
259 |
180 258
|
unssd |
⊢ ( 𝜑 → ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) ) |
260 |
|
fiss |
⊢ ( ( ( MetOpen ‘ 𝐷 ) ∈ Top ∧ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ⊆ ( MetOpen ‘ 𝐷 ) ) → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) ) |
261 |
157 259 260
|
syl2anc |
⊢ ( 𝜑 → ( fi ‘ ( { X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) } ∪ ran ( 𝑚 ∈ 𝐼 , 𝑢 ∈ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑚 ) ↦ ( ◡ ( 𝑤 ∈ X 𝑛 ∈ 𝐼 ∪ ( ( TopOpen ∘ 𝑅 ) ‘ 𝑛 ) ↦ ( 𝑤 ‘ 𝑚 ) ) “ 𝑢 ) ) ) ) ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) ) |
262 |
154 261
|
eqsstrd |
⊢ ( 𝜑 → 𝐶 ⊆ ( fi ‘ ( MetOpen ‘ 𝐷 ) ) ) |
263 |
|
fitop |
⊢ ( ( MetOpen ‘ 𝐷 ) ∈ Top → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) ) |
264 |
157 263
|
syl |
⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( MetOpen ‘ 𝐷 ) ) |
265 |
155
|
mopnval |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝐵 ) → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
266 |
21 265
|
syl |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) ) |
267 |
|
tgdif0 |
⊢ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ ran ( ball ‘ 𝐷 ) ) |
268 |
266 267
|
eqtr4di |
⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) |
269 |
264 268
|
eqtrd |
⊢ ( 𝜑 → ( fi ‘ ( MetOpen ‘ 𝐷 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) |
270 |
262 269
|
sseqtrd |
⊢ ( 𝜑 → 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) |
271 |
|
2basgen |
⊢ ( ( ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ⊆ 𝐶 ∧ 𝐶 ⊆ ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) ) |
272 |
137 270 271
|
syl2anc |
⊢ ( 𝜑 → ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) = ( topGen ‘ 𝐶 ) ) |
273 |
19 272
|
eqtr4d |
⊢ ( 𝜑 → ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) = ( topGen ‘ ( ran ( ball ‘ 𝐷 ) ∖ { ∅ } ) ) ) |
274 |
1 2 3 13 7
|
prdstopn |
⊢ ( 𝜑 → 𝐽 = ( ∏t ‘ ( TopOpen ∘ 𝑅 ) ) ) |
275 |
273 274 268
|
3eqtr4d |
⊢ ( 𝜑 → 𝐽 = ( MetOpen ‘ 𝐷 ) ) |