metcnp2

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . The distance arguments are swapped compared to metcnp (and Munkres' metcn ) for compatibility with df-lm . Definition 1.3-3 of Kreyszig p. 20. (Contributed by NM, 4-Jun-2007) (Revised by Mario Carneiro, 13-Nov-2013)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
Assertion	metcnp2	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (w C P < z \to F (w) D F (P) < y)))$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3	1 2	metcnp	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y)))$
4		simpl1	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to C \in ∞Met (X)$
5	4	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to C \in ∞Met (X)$
6		simpl3	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to P \in X$
7	6	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to P \in X$
8		simpr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to w \in X$
9		xmetsym	$⊢ (C \in ∞Met (X) \land P \in X \land w \in X) \to P C w = w C P$
10	5 7 8 9	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to P C w = w C P$
11	10	breq1d	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to (P C w < z \leftrightarrow w C P < z)$
12		simpl2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to D \in ∞Met (Y)$
13	12	ad2antrr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to D \in ∞Met (Y)$
14		simpllr	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to F : X ⟶ Y$
15	14 7	ffvelrnd	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to F (P) \in Y$
16	14 8	ffvelrnd	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to F (w) \in Y$
17		xmetsym	$⊢ (D \in ∞Met (Y) \land F (P) \in Y \land F (w) \in Y) \to F (P) D F (w) = F (w) D F (P)$
18	13 15 16 17	syl3anc	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to F (P) D F (w) = F (w) D F (P)$
19	18	breq1d	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to (F (P) D F (w) < y \leftrightarrow F (w) D F (P) < y)$
20	11 19	imbi12d	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \land w \in X) \to ((P C w < z \to F (P) D F (w) < y) \leftrightarrow (w C P < z \to F (w) D F (P) < y))$
21	20	ralbidva	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (\forall w \in X (P C w < z \to F (P) D F (w) < y) \leftrightarrow \forall w \in X (w C P < z \to F (w) D F (P) < y))$
22	21	anassrs	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \land z \in ℝ^{+}) \to (\forall w \in X (P C w < z \to F (P) D F (w) < y) \leftrightarrow \forall w \in X (w C P < z \to F (w) D F (P) < y))$
23	22	rexbidva	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land y \in ℝ^{+}) \to (\exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y) \leftrightarrow \exists z \in ℝ^{+} \forall w \in X (w C P < z \to F (w) D F (P) < y))$
24	23	ralbidva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y) \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (w C P < z \to F (w) D F (P) < y))$
25	24	pm5.32da	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to ((F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y)) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (w C P < z \to F (w) D F (P) < y)))$
26	3 25	bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (w C P < z \to F (w) D F (P) < y)))$

Metamath Proof Explorer

Theorem metcnp2

Proof