metcnp

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . (Contributed by NM, 11-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3	1 2	metcnp3	$⊢ (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 ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y))$
4		ffun	$⊢ F : X ⟶ Y \to Fun F$
5	4	ad2antlr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to Fun F$
6		simpll1	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to C \in ∞Met (X)$
7		simpll3	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to P \in X$
8		rpxr	$⊢ z \in ℝ^{+} \to z \in ℝ^{*}$
9	8	ad2antll	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to z \in ℝ^{*}$
10		blssm	$⊢ (C \in ∞Met (X) \land P \in X \land z \in ℝ^{*}) \to P ball (C) z \subseteq X$
11	6 7 9 10	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to P ball (C) z \subseteq X$
12		fdm	$⊢ F : X ⟶ Y \to dom F = X$
13	12	ad2antlr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to dom F = X$
14	11 13	sseqtrrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to P ball (C) z \subseteq dom F$
15		funimass4	$⊢ (Fun F \land P ball (C) z \subseteq dom F) \to (F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \forall w \in (P ball (C) z) F (w) \in (F (P) ball (D) y))$
16	5 14 15	syl2anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \forall w \in (P ball (C) z) F (w) \in (F (P) ball (D) y))$
17		elbl	$⊢ (C \in ∞Met (X) \land P \in X \land z \in ℝ^{*}) \to (w \in (P ball (C) z) \leftrightarrow (w \in X \land P C w < z))$
18	6 7 9 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 ℝ^{+})) \to (w \in (P ball (C) z) \leftrightarrow (w \in X \land P C w < z))$
19	18	imbi1d	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((w \in (P ball (C) z) \to F (w) \in (F (P) ball (D) y)) \leftrightarrow ((w \in X \land P C w < z) \to F (w) \in (F (P) ball (D) y)))$
20		impexp	$⊢ ((w \in X \land P C w < z) \to F (w) \in (F (P) ball (D) y)) \leftrightarrow (w \in X \to (P C w < z \to F (w) \in (F (P) ball (D) y)))$
21		simpl2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \to D \in ∞Met (Y)$
22	21	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)$
23		simplrl	$⊢ ((((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 y \in ℝ^{+}$
24	23	rpxrd	$⊢ ((((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 y \in ℝ^{*}$
25		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$
26	7	adantr	$⊢ ((((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$
27	25 26	ffvelcdmd	$⊢ ((((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$
28		simplr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to F : X ⟶ Y$
29	28	ffvelcdmda	$⊢ ((((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$
30		elbl2	$⊢ ((D \in ∞Met (Y) \land y \in ℝ^{*}) \land (F (P) \in Y \land F (w) \in Y)) \to (F (w) \in (F (P) ball (D) y) \leftrightarrow F (P) D F (w) < y)$
31	22 24 27 29 30	syl22anc	$⊢ ((((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 (F (P) ball (D) y) \leftrightarrow F (P) D F (w) < y)$
32	31	imbi2d	$⊢ ((((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 (w) \in (F (P) ball (D) y)) \leftrightarrow (P C w < z \to F (P) D F (w) < y))$
33	32	pm5.74da	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((w \in X \to (P C w < z \to F (w) \in (F (P) ball (D) y))) \leftrightarrow (w \in X \to (P C w < z \to F (P) D F (w) < y)))$
34	20 33	bitrid	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (((w \in X \land P C w < z) \to F (w) \in (F (P) ball (D) y)) \leftrightarrow (w \in X \to (P C w < z \to F (P) D F (w) < y)))$
35	19 34	bitrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to ((w \in (P ball (C) z) \to F (w) \in (F (P) ball (D) y)) \leftrightarrow (w \in X \to (P C w < z \to F (P) D F (w) < y)))$
36	35	ralbidv2	$⊢ (((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 (P ball (C) z) F (w) \in (F (P) ball (D) y) \leftrightarrow \forall w \in X (P C w < z \to F (P) D F (w) < y))$
37	16 36	bitrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in ℝ^{+} \land z \in ℝ^{+})) \to (F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \forall w \in X (P C w < z \to F (P) D F (w) < y))$
38	37	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 (F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \forall w \in X (P C w < z \to F (P) D F (w) < y))$
39	38	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 ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y))$
40	39	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 ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in X (P C w < z \to F (P) D F (w) < y))$
41	40	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 ℝ^{+} F [P ball (C) z] \subseteq F (P) ball (D) y) \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)))$
42	3 41	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 (P C w < z \to F (P) D F (w) < y)))$

Metamath Proof Explorer

Theorem metcnp

Proof