Step |
Hyp |
Ref |
Expression |
1 |
|
cnmpt1ds.d |
⊢ 𝐷 = ( dist ‘ 𝐺 ) |
2 |
|
cnmpt1ds.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
3 |
|
cnmpt1ds.r |
⊢ 𝑅 = ( topGen ‘ ran (,) ) |
4 |
|
cnmpt1ds.g |
⊢ ( 𝜑 → 𝐺 ∈ MetSp ) |
5 |
|
cnmpt1ds.k |
⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) |
6 |
|
cnmpt1ds.a |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) |
7 |
|
cnmpt1ds.b |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) |
8 |
|
mstps |
⊢ ( 𝐺 ∈ MetSp → 𝐺 ∈ TopSp ) |
9 |
4 8
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ TopSp ) |
10 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
11 |
10 2
|
istps |
⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
12 |
9 11
|
sylib |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ) |
13 |
|
cnf2 |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
14 |
5 12 6 13
|
syl3anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
15 |
14
|
fvmptelrn |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) ) |
16 |
|
cnf2 |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
17 |
5 12 7 16
|
syl3anc |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ ( Base ‘ 𝐺 ) ) |
18 |
17
|
fvmptelrn |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ( Base ‘ 𝐺 ) ) |
19 |
15 18
|
ovresd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) = ( 𝐴 𝐷 𝐵 ) ) |
20 |
19
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐷 𝐵 ) ) ) |
21 |
10 1 2 3
|
msdcn |
⊢ ( 𝐺 ∈ MetSp → ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝑅 ) ) |
22 |
4 21
|
syl |
⊢ ( 𝜑 → ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝑅 ) ) |
23 |
5 6 7 22
|
cnmpt12f |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 ( 𝐷 ↾ ( ( Base ‘ 𝐺 ) × ( Base ‘ 𝐺 ) ) ) 𝐵 ) ) ∈ ( 𝐾 Cn 𝑅 ) ) |
24 |
20 23
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐷 𝐵 ) ) ∈ ( 𝐾 Cn 𝑅 ) ) |