txmetcn

Description: Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		metcn.2	$⊢ J = MetOpen (C)$
2		metcn.4	$⊢ K = MetOpen (D)$
3		txmetcnp.4	$⊢ L = MetOpen (E)$
4	1	mopntopon	$⊢ C \in ∞Met (X) \to J \in TopOn (X)$
5	2	mopntopon	$⊢ D \in ∞Met (Y) \to K \in TopOn (Y)$
6		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
7	4 5 6	syl2an	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
8	7	3adant3	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \to J \times_{t} K \in TopOn (X \times Y)$
9	3	mopntopon	$⊢ E \in ∞Met (Z) \to L \in TopOn (Z)$
10	9	3ad2ant3	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \to L \in TopOn (Z)$
11		cncnp	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (Z)) \to (F \in ((J \times_{t} K) Cn L) \leftrightarrow (F : X \times Y ⟶ Z \land \forall t \in (X \times Y) F \in ((J \times_{t} K) CnP L) (t)))$
12	8 10 11	syl2anc	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \to (F \in ((J \times_{t} K) Cn L) \leftrightarrow (F : X \times Y ⟶ Z \land \forall t \in (X \times Y) F \in ((J \times_{t} K) CnP L) (t)))$
13		fveq2	$⊢ t = ⟨x, y⟩ \to ((J \times_{t} K) CnP L) (t) = ((J \times_{t} K) CnP L) (⟨x, y⟩)$
14	13	eleq2d	$⊢ t = ⟨x, y⟩ \to (F \in ((J \times_{t} K) CnP L) (t) \leftrightarrow F \in ((J \times_{t} K) CnP L) (⟨x, y⟩))$
15	14	ralxp	$⊢ \forall t \in (X \times Y) F \in ((J \times_{t} K) CnP L) (t) \leftrightarrow \forall x \in X \forall y \in Y F \in ((J \times_{t} K) CnP L) (⟨x, y⟩)$
16		simplr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land F : X \times Y ⟶ Z) \land (x \in X \land y \in Y)) \to F : X \times Y ⟶ Z$
17	1 2 3	txmetcnp	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land (x \in X \land y \in Y)) \to (F \in ((J \times_{t} K) CnP L) (⟨x, y⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z)))$
18	17	adantlr	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land F : X \times Y ⟶ Z) \land (x \in X \land y \in Y)) \to (F \in ((J \times_{t} K) CnP L) (⟨x, y⟩) \leftrightarrow (F : X \times Y ⟶ Z \land \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z)))$
19	16 18	mpbirand	$⊢ (((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land F : X \times Y ⟶ Z) \land (x \in X \land y \in Y)) \to (F \in ((J \times_{t} K) CnP L) (⟨x, y⟩) \leftrightarrow \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z))$
20	19	2ralbidva	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land F : X \times Y ⟶ Z) \to (\forall x \in X \forall y \in Y F \in ((J \times_{t} K) CnP L) (⟨x, y⟩) \leftrightarrow \forall x \in X \forall y \in Y \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z))$
21	15 20	syl5bb	$⊢ ((C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \land F : X \times Y ⟶ Z) \to (\forall t \in (X \times Y) F \in ((J \times_{t} K) CnP L) (t) \leftrightarrow \forall x \in X \forall y \in Y \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z))$
22	21	pm5.32da	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \to ((F : X \times Y ⟶ Z \land \forall t \in (X \times Y) F \in ((J \times_{t} K) CnP L) (t)) \leftrightarrow (F : X \times Y ⟶ Z \land \forall x \in X \forall y \in Y \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z)))$
23	12 22	bitrd	$⊢ (C \in ∞Met (X) \land D \in ∞Met (Y) \land E \in ∞Met (Z)) \to (F \in ((J \times_{t} K) Cn L) \leftrightarrow (F : X \times Y ⟶ Z \land \forall x \in X \forall y \in Y \forall z \in ℝ^{+} \exists w \in ℝ^{+} \forall u \in X \forall v \in Y ((x C u < w \land y D v < w) \to (x F y) E (u F v) < z)))$

Metamath Proof Explorer

Theorem txmetcn

Proof