cnmpt2ds

Description: Continuity of the metric function; analogue of cnmpt22f 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)$
	cnmpt2ds.l	$⊢ φ \to L \in TopOn (Y)$
	cnmpt2ds.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
	cnmpt2ds.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
Assertion	cnmpt2ds	$⊢ φ \to (x \in X, y \in Y ⟼ A D B) \in ((K \times_{t} L) 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		cnmpt2ds.l	$⊢ φ \to L \in TopOn (Y)$
7		cnmpt2ds.a	$⊢ φ \to (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)$
8		cnmpt2ds.b	$⊢ φ \to (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)$
9		txtopon	$⊢ (K \in TopOn (X) \land L \in TopOn (Y)) \to K \times_{t} L \in TopOn (X \times Y)$
10	5 6 9	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (X \times Y)$
11		mstps	$⊢ G \in MetSp \to G \in TopSp$
12	4 11	syl	$⊢ φ \to G \in TopSp$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14	13 2	istps	$⊢ G \in TopSp \leftrightarrow J \in TopOn ({Base}_{G})$
15	12 14	sylib	$⊢ φ \to J \in TopOn ({Base}_{G})$
16		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{G}) \land (x \in X, y \in Y ⟼ A) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
17	10 15 7 16	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
18		eqid	$⊢ (x \in X, y \in Y ⟼ A) = (x \in X, y \in Y ⟼ A)$
19	18	fmpo	$⊢ \forall x \in X \forall y \in Y A \in {Base}_{G} \leftrightarrow (x \in X, y \in Y ⟼ A) : X \times Y ⟶ {Base}_{G}$
20	17 19	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y A \in {Base}_{G}$
21	20	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y A \in {Base}_{G}$
22	21	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to A \in {Base}_{G}$
23		cnf2	$⊢ (K \times_{t} L \in TopOn (X \times Y) \land J \in TopOn ({Base}_{G}) \land (x \in X, y \in Y ⟼ B) \in ((K \times_{t} L) Cn J)) \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
24	10 15 8 23	syl3anc	$⊢ φ \to (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
25		eqid	$⊢ (x \in X, y \in Y ⟼ B) = (x \in X, y \in Y ⟼ B)$
26	25	fmpo	$⊢ \forall x \in X \forall y \in Y B \in {Base}_{G} \leftrightarrow (x \in X, y \in Y ⟼ B) : X \times Y ⟶ {Base}_{G}$
27	24 26	sylibr	$⊢ φ \to \forall x \in X \forall y \in Y B \in {Base}_{G}$
28	27	r19.21bi	$⊢ (φ \land x \in X) \to \forall y \in Y B \in {Base}_{G}$
29	28	r19.21bi	$⊢ ((φ \land x \in X) \land y \in Y) \to B \in {Base}_{G}$
30	22 29	ovresd	$⊢ ((φ \land x \in X) \land y \in Y) \to A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B = A D B$
31	30	3impa	$⊢ (φ \land x \in X \land y \in Y) \to A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B = A D B$
32	31	mpoeq3dva	$⊢ φ \to (x \in X, y \in Y ⟼ A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B) = (x \in X, y \in Y ⟼ A D B)$
33	13 1 2 3	msdcn	$⊢ G \in MetSp \to {D ↾}_{({Base}_{G} \times {Base}_{G})} \in ((J \times_{t} J) Cn R)$
34	4 33	syl	$⊢ φ \to {D ↾}_{({Base}_{G} \times {Base}_{G})} \in ((J \times_{t} J) Cn R)$
35	5 6 7 8 34	cnmpt22f	$⊢ φ \to (x \in X, y \in Y ⟼ A ({D ↾}_{({Base}_{G} \times {Base}_{G})}) B) \in ((K \times_{t} L) Cn R)$
36	32 35	eqeltrrd	$⊢ φ \to (x \in X, y \in Y ⟼ A D B) \in ((K \times_{t} L) Cn R)$

Metamath Proof Explorer

Theorem cnmpt2ds

Proof