metcnpi2

Description: Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 . (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	metcnpi2	$⊢ ((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 < x \to F (y) D F (P) < 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	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 z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (y C P < x \to F (y) D F (P) < 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 (y C P < x \to F (y) D F (P) < 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 (y C P < x \to F (y) D F (P) < z))$
15		breq2	$⊢ z = A \to (F (y) D F (P) < z \leftrightarrow F (y) D F (P) < A)$
16	15	imbi2d	$⊢ z = A \to ((y C P < x \to F (y) D F (P) < z) \leftrightarrow (y C P < x \to F (y) D F (P) < A))$
17	16	rexralbidv	$⊢ z = A \to (\exists x \in ℝ^{+} \forall y \in X (y C P < x \to F (y) D F (P) < z) \leftrightarrow \exists x \in ℝ^{+} \forall y \in X (y C P < x \to F (y) D F (P) < A))$
18	17	rspccv	$⊢ \forall z \in ℝ^{+} \exists x \in ℝ^{+} \forall y \in X (y C P < x \to F (y) D F (P) < z) \to (A \in ℝ^{+} \to \exists x \in ℝ^{+} \forall y \in X (y C P < x \to F (y) D F (P) < 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 (y C P < x \to F (y) D F (P) < 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 (y C P < x \to F (y) D F (P) < A)$

Metamath Proof Explorer

Theorem metcnpi2

Proof