Metamath Proof Explorer

Theorem metcnp

Description: Two ways to say a mapping from metric C to metric D is continuous at point P . (Contributed by NM, 11-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
Assertion metcnp ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
2 metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
3 1 2 metcnp3 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
4 ffun ⊒ ( 𝐹 : 𝑋 ⟢ π‘Œ β†’ Fun 𝐹 )
5 4 ad2antlr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ Fun 𝐹 )
6 simpll1 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) )
7 simpll3 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ 𝑃 ∈ 𝑋 )
8 rpxr ⊒ ( 𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ* )
9 8 ad2antll ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ 𝑧 ∈ ℝ* )
10 blssm ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) β†’ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑋 )
11 6 7 9 10 syl3anc ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑋 )
12 fdm ⊒ ( 𝐹 : 𝑋 ⟢ π‘Œ β†’ dom 𝐹 = 𝑋 )
13 12 ad2antlr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ dom 𝐹 = 𝑋 )
14 11 13 sseqtrrd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† dom 𝐹 )
15 funimass4 ⊒ ( ( Fun 𝐹 ∧ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† dom 𝐹 ) β†’ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
16 5 14 15 syl2anc ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
17 elbl ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) β†’ ( 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑃 𝐢 𝑀 ) < 𝑧 ) ) )
18 6 7 9 17 syl3anc ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ↔ ( 𝑀 ∈ 𝑋 ∧ ( 𝑃 𝐢 𝑀 ) < 𝑧 ) ) )
19 18 imbi1d ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( ( 𝑀 ∈ 𝑋 ∧ ( 𝑃 𝐢 𝑀 ) < 𝑧 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
20 impexp ⊒ ( ( ( 𝑀 ∈ 𝑋 ∧ ( 𝑃 𝐢 𝑀 ) < 𝑧 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( 𝑀 ∈ 𝑋 β†’ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
21 simpl2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) )
22 21 ad2antrr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) )
23 simplrl ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ 𝑦 ∈ ℝ+ )
24 23 rpxrd ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ 𝑦 ∈ ℝ* )
25 simpllr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
26 7 adantr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ 𝑃 ∈ 𝑋 )
27 25 26 ffvelcdmd ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ )
28 simplr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
29 28 ffvelcdmda ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ π‘Œ )
30 elbl2 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑦 ∈ ℝ* ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ ∧ ( 𝐹 β€˜ 𝑀 ) ∈ π‘Œ ) ) β†’ ( ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) )
31 22 24 27 29 30 syl22anc ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ ( ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) )
32 31 imbi2d ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑀 ∈ 𝑋 ) β†’ ( ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
33 32 pm5.74da ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( 𝑀 ∈ 𝑋 β†’ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) ↔ ( 𝑀 ∈ 𝑋 β†’ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
34 20 33 bitrid ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( ( 𝑀 ∈ 𝑋 ∧ ( 𝑃 𝐢 𝑀 ) < 𝑧 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( 𝑀 ∈ 𝑋 β†’ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
35 19 34 bitrd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( 𝑀 ∈ 𝑋 β†’ ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
36 35 ralbidv2 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( βˆ€ 𝑀 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ( 𝐹 β€˜ 𝑀 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
37 16 36 bitrd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) ) β†’ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
38 37 anassrs ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ 𝑧 ∈ ℝ+ ) β†’ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
39 38 rexbidva ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
40 39 ralbidva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ↔ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) )
41 40 pm5.32da ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )
42 3 41 bitrd ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ βˆ€ 𝑀 ∈ 𝑋 ( ( 𝑃 𝐢 𝑀 ) < 𝑧 β†’ ( ( 𝐹 β€˜ 𝑃 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < 𝑦 ) ) ) )