Metamath Proof Explorer


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 syl5bb ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞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 𝐿 ) β€˜ ⟨ 𝐴 , 𝐡 ⟩ ) ↔ ( 𝐹 : ( 𝑋 Γ— π‘Œ ) ⟢ 𝑍 ∧ βˆ€ 𝑧 ∈ ℝ+ βˆƒ 𝑀 ∈ ℝ+ βˆ€ 𝑒 ∈ 𝑋 βˆ€ 𝑣 ∈ π‘Œ ( ( ( 𝐴 𝐢 𝑒 ) < 𝑀 ∧ ( 𝐡 𝐷 𝑣 ) < 𝑀 ) β†’ ( ( 𝐴 𝐹 𝐡 ) 𝐸 ( 𝑒 𝐹 𝑣 ) ) < 𝑧 ) ) ) )