Theorem txmetcn

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

	Ref	Expression
Hypotheses	metcn.2	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
	metcn.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
	txmetcnp.4	⊢ 𝐿 = ( MetOpen ‘ 𝐸 )
Assertion	txmetcn	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metcn.2	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2		metcn.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3		txmetcnp.4	⊢ 𝐿 = ( MetOpen ‘ 𝐸 )
4	1	mopntopon	⊢ ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5	2	mopntopon	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
6		txtopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
7	4 5 6	syl2an	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
8	7	3adant3	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
9	3	mopntopon	⊢ ( 𝐸 ∈ ( ∞Met ‘ 𝑍 ) → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
10	9	3ad2ant3	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → 𝐿 ∈ ( TopOn ‘ 𝑍 ) )
11		cncnp	⊢ ( ( ( 𝐽 ×t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑍 ) ) → ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑡 ∈ ( 𝑋 × 𝑌 ) 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ) ) )
12	8 10 11	syl2anc	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑡 ∈ ( 𝑋 × 𝑌 ) 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ) ) )
13		fveq2	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) = ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14	13	eleq2d	⊢ ( 𝑡 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ↔ 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
15	14	ralxp	⊢ ( ∀ 𝑡 ∈ ( 𝑋 × 𝑌 ) 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
16		simplr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
17	1 2 3	txmetcnp	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )
18	17	adantlr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )
19	16 18	mpbirand	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
20	19	2ralbidva	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
21	15 20	syl5bb	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) → ( ∀ 𝑡 ∈ ( 𝑋 × 𝑌 ) 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
22	21	pm5.32da	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → ( ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑡 ∈ ( 𝑋 × 𝑌 ) 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ 𝑡 ) ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )
23	12 22	bitrd	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) → ( 𝐹 ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐿 ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝑥 𝐶 𝑢 ) < 𝑤 ∧ ( 𝑦 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝑥 𝐹 𝑦 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )