metcn

Description: Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of Munkres p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D . (Contributed by NM, 15-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3	1	mopntopon	$⊢ C \in ∞Met (X) \to J \in TopOn (X)$
4	2	mopntopon	$⊢ D \in ∞Met (Y) \to K \in TopOn (Y)$
5		cncnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x)))$
6	3 4 5	syl2an	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x)))$
7		simplr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F : X ⟶ Y) \land x \in X) \to F : X ⟶ Y$
8	1 2	metcnp	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land x \in X) \to (F \in (J CnP K) (x) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y)))$
9	8	ad4ant124	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F : X ⟶ Y) \land x \in X) \to (F \in (J CnP K) (x) \leftrightarrow (F : X ⟶ Y \land \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y)))$
10	7 9	mpbirand	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F : X ⟶ Y) \land x \in X) \to (F \in (J CnP K) (x) \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y))$
11	10	ralbidva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F : X ⟶ Y) \to (\forall x \in X F \in (J CnP K) (x) \leftrightarrow \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y))$
12	11	pm5.32da	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y)) \to ((F : X ⟶ Y \land \forall x \in X F \in (J CnP K) (x)) \leftrightarrow (F : X ⟶ Y \land \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y)))$
13	6 12	bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y)) \to (F \in (J Cn K) \leftrightarrow (F : X ⟶ Y \land \forall x \in X \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (x C w < z \to F (x) D F (w) < y)))$

Metamath Proof Explorer

Theorem metcn

Proof