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	$⊢ φ \to G \in MetSp$
	cnmpt1ds.k	$⊢ φ \to K \in TopOn (X)$
	cnmpt1ds.a	$⊢ φ \to (x \in X ⟼ A) \in (K Cn J)$
	cnmpt1ds.b	$⊢ φ \to (x \in X ⟼ B) \in (K Cn J)$
Assertion	cnmpt1ds	$⊢ φ \to (x \in X ⟼ A D B) \in (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	$⊢ φ \to G \in MetSp$
5		cnmpt1ds.k	$⊢ φ \to K \in TopOn (X)$
6		cnmpt1ds.a	$⊢ φ \to (x \in X ⟼ A) \in (K Cn J)$
7		cnmpt1ds.b	$⊢ φ \to (x \in X ⟼ B) \in (K Cn J)$
8		mstps	$⊢ G \in MetSp \to G \in TopSp$
9	4 8	syl	$⊢ φ \to G \in TopSp$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	10 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn ({Base}_{G})$
12	9 11	sylib	$⊢ φ \to J \in TopOn ({Base}_{G})$
13		cnf2	$⊢ (K \in TopOn (X) \land J \in TopOn ({Base}_{G}) \land (x \in X ⟼ A) \in (K Cn J)) \to (x \in X ⟼ A) : X ⟶ {Base}_{G}$
14	5 12 6 13	syl3anc	$⊢ φ \to (x \in X ⟼ A) : X ⟶ {Base}_{G}$
15	14	fvmptelcdm	$⊢ (φ \land x \in X) \to A \in {Base}_{G}$
16		cnf2	$⊢ (K \in TopOn (X) \land J \in TopOn ({Base}_{G}) \land (x \in X ⟼ B) \in (K Cn J)) \to (x \in X ⟼ B) : X ⟶ {Base}_{G}$
17	5 12 7 16	syl3anc	$⊢ φ \to (x \in X ⟼ B) : X ⟶ {Base}_{G}$
18	17	fvmptelcdm	$⊢ (φ \land x \in X) \to B \in {Base}_{G}$
19	15 18	ovresd	$⊢ (φ \land x \in X) \to A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B = A D B$
20	19	mpteq2dva	$⊢ φ \to (x \in X ⟼ A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B) = (x \in X ⟼ A D B)$
21	10 1 2 3	msdcn	$⊢ G \in MetSp \to {D ↾}_{({Base}_{G} \times {Base}_{G})} \in ((J \times_{t} J) Cn R)$
22	4 21	syl	$⊢ φ \to {D ↾}_{({Base}_{G} \times {Base}_{G})} \in ((J \times_{t} J) Cn R)$
23	5 6 7 22	cnmpt12f	$⊢ φ \to (x \in X ⟼ A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B) \in (K Cn R)$
24	20 23	eqeltrrd	$⊢ φ \to (x \in X ⟼ A D B) \in (K Cn R)$

Metamath Proof Explorer

Theorem cnmpt1ds

Proof