Metamath Proof Explorer

Theorem cnmpt1ds

Description: Continuity of the metric function; analogue of cnmpt12f which cannot be used directly because D is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Hypotheses cnmpt1ds.d ⊢ D = dist ⁡ G
cnmpt1ds.j ⊢ J = TopOpen ⁡ G
cnmpt1ds.r ⊢ R = topGen ⁡ ran ⁡ .
cnmpt1ds.g ⊢ φ → G ∈ MetSp
cnmpt1ds.k ⊢ φ → K ∈ TopOn ⁡ X
cnmpt1ds.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
cnmpt1ds.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
Assertion cnmpt1ds ⊢ φ → x ∈ X ⟼ A D B ∈ K Cn R

Proof

Step Hyp Ref Expression
1 cnmpt1ds.d ⊢ D = dist ⁡ G
2 cnmpt1ds.j ⊢ J = TopOpen ⁡ G
3 cnmpt1ds.r ⊢ R = topGen ⁡ ran ⁡ .
4 cnmpt1ds.g ⊢ φ → G ∈ MetSp
5 cnmpt1ds.k ⊢ φ → K ∈ TopOn ⁡ X
6 cnmpt1ds.a ⊢ φ → x ∈ X ⟼ A ∈ K Cn J
7 cnmpt1ds.b ⊢ φ → x ∈ X ⟼ B ∈ K Cn J
8 mstps ⊢ G ∈ MetSp → G ∈ TopSp
9 4 8 syl ⊢ φ → G ∈ TopSp
10 eqid ⊢ Base G = Base G
11 10 2 istps ⊢ G ∈ TopSp ↔ J ∈ TopOn ⁡ Base G
12 9 11 sylib ⊢ φ → J ∈ TopOn ⁡ Base G
13 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base G ∧ x ∈ X ⟼ A ∈ K Cn J → x ∈ X ⟼ A : X ⟶ Base G
14 5 12 6 13 syl3anc ⊢ φ → x ∈ X ⟼ A : X ⟶ Base G
15 14 fvmptelrn ⊢ φ ∧ x ∈ X → A ∈ Base G
16 cnf2 ⊢ K ∈ TopOn ⁡ X ∧ J ∈ TopOn ⁡ Base G ∧ x ∈ X ⟼ B ∈ K Cn J → x ∈ X ⟼ B : X ⟶ Base G
17 5 12 7 16 syl3anc ⊢ φ → x ∈ X ⟼ B : X ⟶ Base G
18 17 fvmptelrn ⊢ φ ∧ x ∈ X → B ∈ Base G
19 15 18 ovresd ⊢ φ ∧ x ∈ X → A D ↾ Base G × Base G B = A D B
20 19 mpteq2dva ⊢ φ → x ∈ X ⟼ A D ↾ Base G × Base G B = x ∈ X ⟼ A D B
21 10 1 2 3 msdcn ⊢ G ∈ MetSp → D ↾ Base G × Base G ∈ J × t J Cn R
22 4 21 syl ⊢ φ → D ↾ Base G × Base G ∈ J × t J Cn R
23 5 6 7 22 cnmpt12f ⊢ φ → x ∈ X ⟼ A D ↾ Base G × Base G B ∈ K Cn R
24 20 23 eqeltrrd ⊢ φ → x ∈ X ⟼ A D B ∈ K Cn R