metcnpi

Description: Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp . (Contributed by NM, 17-Dec-2007) (Revised by Mario Carneiro, 13-Nov-2013)

	Ref	Expression
Hypotheses	metcn.2	$⊢ J = MetOpen (C)$
	metcn.4	$⊢ K = MetOpen (D)$
Assertion	metcnpi	$⊢ ((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 (P C y < x \to F (P) D F (y) < A)$

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3		simpr	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to F \in (J CnP K) (P)$
4		simpll	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to C \in ∞Met (X)$
5		simplr	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to D \in ∞Met (Y)$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	cnprcl	$⊢ F \in (J CnP K) (P) \to P \in ⋃ J$
8	7	adantl	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to P \in ⋃ J$
9	1	mopnuni	$⊢ C \in ∞Met (X) \to X = ⋃ J$
10	9	ad2antrr	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to X = ⋃ J$
11	8 10	eleqtrrd	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to P \in X$
12	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 z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < z)))$
13	4 5 11 12	syl3anc	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < z)))$
14	3 13	mpbid	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to (F : X ⟶ Y \land \forall z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < z))$
15		breq2	$⊢ z = A \to (F (P) D F (y) < z \leftrightarrow F (P) D F (y) < A)$
16	15	imbi2d	$⊢ z = A \to ((P C y < x \to F (P) D F (y) < z) \leftrightarrow (P C y < x \to F (P) D F (y) < A))$
17	16	rexralbidv	$⊢ z = A \to (\exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < z) \leftrightarrow \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < A))$
18	17	rspccv	$⊢ \forall z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < z) \to (A \in ℝ^{+} \to \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < A))$
19	14 18	simpl2im	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y)) \land F \in (J CnP K) (P)) \to (A \in ℝ^{+} \to \exists x \in ℝ^{+} \forall y \in X (P C y < x \to F (P) D F (y) < A))$
20	19	impr	$⊢ ((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 (P C y < x \to F (P) D F (y) < A)$

Metamath Proof Explorer

Theorem metcnpi

Proof