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 𝐷 = ( dist ‘ 𝐺 )
cnmpt1ds.j 𝐽 = ( TopOpen ‘ 𝐺 )
cnmpt1ds.r 𝑅 = ( topGen ‘ ran (,) )
cnmpt1ds.g ( 𝜑𝐺 ∈ MetSp )
cnmpt1ds.k ( 𝜑𝐾 ∈ ( TopOn ‘ 𝑋 ) )
cnmpt1ds.a ( 𝜑 → ( 𝑥𝑋𝐴 ) ∈ ( 𝐾 Cn 𝐽 ) )
cnmpt1ds.b ( 𝜑 → ( 𝑥𝑋𝐵 ) ∈ ( 𝐾 Cn 𝐽 ) )
Assertion cnmpt1ds ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝐴 𝐷 𝐵 ) ) ∈ ( 𝐾 Cn 𝑅 ) )

Proof

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 𝑅 ) )