metcnpi3

Description: Epsilon-delta property of a metric space function continuous at P . A variation of metcnpi2 with non-strict ordering. (Contributed by NM, 16-Dec-2007) (Revised by Mario Carneiro, 13-Nov-2013)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
Assertion	metcnpi3	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \to \exists x \in ℝ^{+} \forall y \in X (y C P \leq x \to F (y) D F (P) \leq A)$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3	1 2	metcnpi2	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall y \in X (y C P < z \to F (y) D F (P) < A)$
4		rphalfcl	$⊢ z \in ℝ^{+} \to \frac{z}{2} \in ℝ^{+}$
5	4	ad2antrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land \forall y \in X (y C P < z \to F (y) D F (P) < A))) \to \frac{z}{2} \in ℝ^{+}$
6		simplll	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to C \in ∞Met (X)$
7		simprr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to y \in X$
8		simplrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to F \in (J CnP K) (P)$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	cnprcl	$⊢ F \in (J CnP K) (P) \to P \in ⋃ J$
11	8 10	syl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to P \in ⋃ J$
12	1	mopnuni	$⊢ C \in ∞Met (X) \to X = ⋃ J$
13	6 12	syl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to X = ⋃ J$
14	11 13	eleqtrrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to P \in X$
15		xmetcl	$⊢ (C \in ∞Met (X) \land y \in X \land P \in X) \to y C P \in ℝ^{*}$
16	6 7 14 15	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to y C P \in ℝ^{*}$
17	4	ad2antrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to \frac{z}{2} \in ℝ^{+}$
18	17	rpxrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to \frac{z}{2} \in ℝ^{*}$
19		rpxr	$⊢ z \in ℝ^{+} \to z \in ℝ^{*}$
20	19	ad2antrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to z \in ℝ^{*}$
21		rphalflt	$⊢ z \in ℝ^{+} \to \frac{z}{2} < z$
22	21	ad2antrl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to \frac{z}{2} < z$
23		xrlelttr	$⊢ (y C P \in ℝ^{} \land \frac{z}{2} \in ℝ^{} \land z \in ℝ^{*}) \to ((y C P \leq \frac{z}{2} \land \frac{z}{2} < z) \to y C P < z)$
24	23	expcomd	$⊢ (y C P \in ℝ^{} \land \frac{z}{2} \in ℝ^{} \land z \in ℝ^{*}) \to (\frac{z}{2} < z \to (y C P \leq \frac{z}{2} \to y C P < z))$
25	24	imp	$⊢ ((y C P \in ℝ^{} \land \frac{z}{2} \in ℝ^{} \land z \in ℝ^{*}) \land \frac{z}{2} < z) \to (y C P \leq \frac{z}{2} \to y C P < z)$
26	16 18 20 22 25	syl31anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to (y C P \leq \frac{z}{2} \to y C P < z)$
27		simpllr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to D \in ∞Met (Y)$
28	1	mopntopon	$⊢ C \in ∞Met (X) \to J \in TopOn (X)$
29	6 28	syl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to J \in TopOn (X)$
30	2	mopntopon	$⊢ D \in ∞Met (Y) \to K \in TopOn (Y)$
31	27 30	syl	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to K \in TopOn (Y)$
32		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
33	29 31 8 32	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to F : X ⟶ Y$
34	33 7	ffvelcdmd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to F (y) \in Y$
35	33 14	ffvelcdmd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to F (P) \in Y$
36		xmetcl	$⊢ (D \in ∞Met (Y) \land F (y) \in Y \land F (P) \in Y) \to F (y) D F (P) \in ℝ^{*}$
37	27 34 35 36	syl3anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to F (y) D F (P) \in ℝ^{*}$
38		simplrr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to A \in ℝ^{+}$
39	38	rpxrd	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to A \in ℝ^{*}$
40		xrltle	$⊢ (F (y) D F (P) \in ℝ^{} \land A \in ℝ^{}) \to (F (y) D F (P) < A \to F (y) D F (P) \leq A)$
41	37 39 40	syl2anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to (F (y) D F (P) < A \to F (y) D F (P) \leq A)$
42	26 41	imim12d	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land y \in X)) \to ((y C P < z \to F (y) D F (P) < A) \to (y C P \leq \frac{z}{2} \to F (y) D F (P) \leq A))$
43	42	anassrs	$⊢ ((((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land z \in ℝ^{+}) \land y \in X) \to ((y C P < z \to F (y) D F (P) < A) \to (y C P \leq \frac{z}{2} \to F (y) D F (P) \leq A))$
44	43	ralimdva	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land z \in ℝ^{+}) \to (\forall y \in X (y C P < z \to F (y) D F (P) < A) \to \forall y \in X (y C P \leq \frac{z}{2} \to F (y) D F (P) \leq A))$
45	44	impr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land \forall y \in X (y C P < z \to F (y) D F (P) < A))) \to \forall y \in X (y C P \leq \frac{z}{2} \to F (y) D F (P) \leq A)$
46		breq2	$⊢ x = \frac{z}{2} \to (y C P \leq x \leftrightarrow y C P \leq \frac{z}{2})$
47	46	rspceaimv	$⊢ (\frac{z}{2} \in ℝ^{+} \land \forall y \in X (y C P \leq \frac{z}{2} \to F (y) D F (P) \leq A)) \to \exists x \in ℝ^{+} \forall y \in X (y C P \leq x \to F (y) D F (P) \leq A)$
48	5 45 47	syl2anc	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \land (z \in ℝ^{+} \land \forall y \in X (y C P < z \to F (y) D F (P) < A))) \to \exists x \in ℝ^{+} \forall y \in X (y C P \leq x \to F (y) D F (P) \leq A)$
49	3 48	rexlimddv	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land (F \in (J CnP K) (P) \land A \in ℝ^{+})) \to \exists x \in ℝ^{+} \forall y \in X (y C P \leq x \to F (y) D F (P) \leq A)$

Metamath Proof Explorer

Theorem metcnpi3

Proof