Theorem txmetcnp

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	txmetcnp	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metcn.2	⊢ 𝐽 = ( MetOpen ‘ 𝐶 )
2		metcn.4	⊢ 𝐾 = ( MetOpen ‘ 𝐷 )
3		txmetcnp.4	⊢ 𝐿 = ( MetOpen ‘ 𝐸 )
4		eqid	⊢ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) = ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) )
5		simpl1	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
6		simpl2	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
7	4 5 6	tmsxps	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) )
8		simpl3	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑍 ) )
9		opelxpi	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
10	9	adantl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) )
11		eqid	⊢ ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) = ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) )
12	11 3	metcnp	⊢ ( ( ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ∈ ( ∞Met ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐹 ∈ ( ( ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ) ) )
13	7 8 10 12	syl3anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ) ) )
14	4 5 6 1 2 11	tmsxpsmopn	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) = ( 𝐽 ×t 𝐾 ) )
15	14	oveq1d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) CnP 𝐿 ) = ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) )
16	15	fveq1d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
17	16	eleq2d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( MetOpen ‘ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
18		oveq2	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) = ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) )
19	18	breq1d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 ) )
20		df-ov	⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
21	20	oveq1i	⊢ ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) )
22		fveq2	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
23		df-ov	⊢ ( 𝑢 𝐹 𝑣 ) = ( 𝐹 ‘ ⟨ 𝑢 , 𝑣 ⟩ )
24	22 23	eqtr4di	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐹 ‘ 𝑥 ) = ( 𝑢 𝐹 𝑣 ) )
25	24	oveq2d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) )
26	21 25	eqtr3id	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) )
27	26	breq1d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ↔ ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) )
28	19 27	imbi12d	⊢ ( 𝑥 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ↔ ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
29	28	ralxp	⊢ ( ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) )
30	5	ad2antrr	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
31	6	ad2antrr	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑌 ) )
32		simpllr	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) )
33	32	simpld	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝐴 ∈ 𝑋 )
34	32	simprd	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝐵 ∈ 𝑌 )
35		simprrl	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝑢 ∈ 𝑋 )
36		simprrr	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝑣 ∈ 𝑌 )
37	4 30 31 33 34 35 36	tmsxpsval2	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) = if ( ( 𝐴 𝐶 𝑢 ) ≤ ( 𝐵 𝐷 𝑣 ) , ( 𝐵 𝐷 𝑣 ) , ( 𝐴 𝐶 𝑢 ) ) )
38	37	breq1d	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 ↔ if ( ( 𝐴 𝐶 𝑢 ) ≤ ( 𝐵 𝐷 𝑣 ) , ( 𝐵 𝐷 𝑣 ) , ( 𝐴 𝐶 𝑢 ) ) < 𝑤 ) )
39		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ) → ( 𝐴 𝐶 𝑢 ) ∈ ℝ* )
40	30 33 35 39	syl3anc	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( 𝐴 𝐶 𝑢 ) ∈ ℝ* )
41		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( 𝐵 𝐷 𝑣 ) ∈ ℝ* )
42	31 34 36 41	syl3anc	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( 𝐵 𝐷 𝑣 ) ∈ ℝ* )
43		rpxr	⊢ ( 𝑤 ∈ ℝ+ → 𝑤 ∈ ℝ* )
44	43	ad2antrl	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → 𝑤 ∈ ℝ* )
45		xrmaxlt	⊢ ( ( ( 𝐴 𝐶 𝑢 ) ∈ ℝ* ∧ ( 𝐵 𝐷 𝑣 ) ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( if ( ( 𝐴 𝐶 𝑢 ) ≤ ( 𝐵 𝐷 𝑣 ) , ( 𝐵 𝐷 𝑣 ) , ( 𝐴 𝐶 𝑢 ) ) < 𝑤 ↔ ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) ) )
46	40 42 44 45	syl3anc	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( if ( ( 𝐴 𝐶 𝑢 ) ≤ ( 𝐵 𝐷 𝑣 ) , ( 𝐵 𝐷 𝑣 ) , ( 𝐴 𝐶 𝑢 ) ) < 𝑤 ↔ ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) ) )
47	38 46	bitrd	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 ↔ ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) ) )
48	47	imbi1d	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ ( 𝑤 ∈ ℝ+ ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ↔ ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
49	48	anassrs	⊢ ( ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ 𝑤 ∈ ℝ+ ) ∧ ( 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑌 ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ↔ ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
50	49	2ralbidva	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) ⟨ 𝑢 , 𝑣 ⟩ ) < 𝑤 → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
51	29 50	bitrid	⊢ ( ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ↔ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
52	51	rexbidva	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
53	52	ralbidv	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ) → ( ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ↔ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) )
54	53	pm5.32da	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝑋 × 𝑌 ) ( ( ⟨ 𝐴 , 𝐵 ⟩ ( dist ‘ ( ( toMetSp ‘ 𝐶 ) ×s ( toMetSp ‘ 𝐷 ) ) ) 𝑥 ) < 𝑤 → ( ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) 𝐸 ( 𝐹 ‘ 𝑥 ) ) < 𝑧 ) ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )
55	13 17 54	3bitr3d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑍 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐹 ∈ ( ( ( 𝐽 ×t 𝐾 ) CnP 𝐿 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝐹 : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ 𝑋 ∀ 𝑣 ∈ 𝑌 ( ( ( 𝐴 𝐶 𝑢 ) < 𝑤 ∧ ( 𝐵 𝐷 𝑣 ) < 𝑤 ) → ( ( 𝐴 𝐹 𝐵 ) 𝐸 ( 𝑢 𝐹 𝑣 ) ) < 𝑧 ) ) ) )