Metamath Proof Explorer

Theorem metcnp3

Description: Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of Gleason p. 240. (Contributed by NM, 17-May-2007) (Revised by Mario Carneiro, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 metcn.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐢 )
2 metcn.4 ⊒ 𝐾 = ( MetOpen β€˜ 𝐷 )
3 1 mopntopon ⊒ ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
4 3 3ad2ant1 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
5 2 mopnval ⊒ ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) β†’ 𝐾 = ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) )
6 5 3ad2ant2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ 𝐾 = ( topGen β€˜ ran ( ball β€˜ 𝐷 ) ) )
7 2 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) β†’ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) )
8 7 3ad2ant2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ 𝐾 ∈ ( TopOn β€˜ π‘Œ ) )
9 simp3 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ 𝑃 ∈ 𝑋 )
10 4 6 8 9 tgcnp ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) ) )
11 simpll2 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) )
12 simplr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝐹 : 𝑋 ⟢ π‘Œ )
13 simpll3 ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝑃 ∈ 𝑋 )
14 12 13 ffvelcdmd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ )
15 simpr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝑦 ∈ ℝ+ )
16 blcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) )
17 11 14 15 16 syl3anc ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) )
18 rpxr ⊒ ( 𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ* )
19 18 adantl ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ 𝑦 ∈ ℝ* )
20 blelrn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ π‘Œ ∧ 𝑦 ∈ ℝ* ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ∈ ran ( ball β€˜ 𝐷 ) )
21 11 14 19 20 syl3anc ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ∈ ran ( ball β€˜ 𝐷 ) )
22 eleq2 ⊒ ( 𝑒 = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ↔ ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
23 sseq2 ⊒ ( 𝑒 = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ↔ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
24 23 anbi2d ⊒ ( 𝑒 = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ↔ ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
25 24 rexbidv ⊒ ( 𝑒 = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ↔ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
26 22 25 imbi12d ⊒ ( 𝑒 = ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ↔ ( ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) ) )
27 26 rspcv ⊒ ( ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ∈ ran ( ball β€˜ 𝐷 ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) ) )
28 21 27 syl ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ∈ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) ) )
29 17 28 mpid ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
30 simpl1 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) )
31 30 ad2antrr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) β†’ 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) )
32 simplrr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) β†’ 𝑣 ∈ 𝐽 )
33 simpr ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) β†’ 𝑃 ∈ 𝑣 )
34 1 mopni2 ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑣 ∈ 𝐽 ∧ 𝑃 ∈ 𝑣 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑣 )
35 31 32 33 34 syl3anc ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑣 )
36 sstr2 ⊒ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( 𝐹 β€œ 𝑣 ) β†’ ( ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
37 imass2 ⊒ ( ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑣 β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( 𝐹 β€œ 𝑣 ) )
38 36 37 syl11 ⊒ ( ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑣 β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
39 38 reximdv ⊒ ( ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) βŠ† 𝑣 β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
40 35 39 syl5com ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) ∧ 𝑃 ∈ 𝑣 ) β†’ ( ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
41 40 expimpd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ ( 𝑦 ∈ ℝ+ ∧ 𝑣 ∈ 𝐽 ) ) β†’ ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
42 41 expr ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( 𝑣 ∈ 𝐽 β†’ ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
43 42 rexlimdv ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
44 29 43 syld ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
45 44 ralrimdva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) β†’ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
46 simpl2 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) )
47 blss ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 )
48 47 3expib ⊒ ( 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) β†’ ( ( 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) )
49 46 48 syl ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( ( 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) )
50 r19.29r ⊒ ( ( βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑦 ∈ ℝ+ ( ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ∧ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
51 30 ad5ant12 ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) )
52 13 ad2antrr ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ 𝑃 ∈ 𝑋 )
53 rpxr ⊒ ( 𝑧 ∈ ℝ+ β†’ 𝑧 ∈ ℝ* )
54 53 ad2antrl ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ 𝑧 ∈ ℝ* )
55 1 blopn ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ* ) β†’ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ∈ 𝐽 )
56 51 52 54 55 syl3anc ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ∈ 𝐽 )
57 simprl ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ 𝑧 ∈ ℝ+ )
58 blcntr ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ ℝ+ ) β†’ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) )
59 51 52 57 58 syl3anc ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) )
60 sstr ⊒ ( ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 )
61 60 ad2ant2l ⊒ ( ( ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ∧ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 )
62 61 ancoms ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 )
63 eleq2 ⊒ ( 𝑣 = ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( 𝑃 ∈ 𝑣 ↔ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) )
64 imaeq2 ⊒ ( 𝑣 = ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( 𝐹 β€œ 𝑣 ) = ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) )
65 64 sseq1d ⊒ ( 𝑣 = ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ↔ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 ) )
66 63 65 anbi12d ⊒ ( 𝑣 = ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) β†’ ( ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 ) ) )
67 66 rspcev ⊒ ( ( ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† 𝑒 ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) )
68 56 59 62 67 syl12anc ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ ( 𝑧 ∈ ℝ+ ∧ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) )
69 68 expr ⊒ ( ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) ∧ 𝑧 ∈ ℝ+ ) β†’ ( ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) )
70 69 rexlimdva ⊒ ( ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ) β†’ ( βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) )
71 70 expimpd ⊒ ( ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) ∧ 𝑦 ∈ ℝ+ ) β†’ ( ( ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ∧ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) )
72 71 rexlimdva ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆƒ 𝑦 ∈ ℝ+ ( ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ∧ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) )
73 50 72 syl5 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( ( βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) )
74 73 expd ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆƒ 𝑦 ∈ ℝ+ ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) βŠ† 𝑒 β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) )
75 49 74 syld ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( ( 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) )
76 75 com23 ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( ( 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ∧ ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 ) β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) )
77 76 exp4a ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ ( 𝑒 ∈ ran ( ball β€˜ 𝐷 ) β†’ ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) ) )
78 77 ralrimdv ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) β†’ βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) )
79 45 78 impbid ⊒ ( ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐹 : 𝑋 ⟢ π‘Œ ) β†’ ( βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ↔ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) )
80 79 pm5.32da ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑒 ∈ ran ( ball β€˜ 𝐷 ) ( ( 𝐹 β€˜ 𝑃 ) ∈ 𝑒 β†’ βˆƒ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 ∧ ( 𝐹 β€œ 𝑣 ) βŠ† 𝑒 ) ) ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )
81 10 80 bitrd ⊒ ( ( 𝐢 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐷 ∈ ( ∞Met β€˜ π‘Œ ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) β€˜ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟢ π‘Œ ∧ βˆ€ 𝑦 ∈ ℝ+ βˆƒ 𝑧 ∈ ℝ+ ( 𝐹 β€œ ( 𝑃 ( ball β€˜ 𝐢 ) 𝑧 ) ) βŠ† ( ( 𝐹 β€˜ 𝑃 ) ( ball β€˜ 𝐷 ) 𝑦 ) ) ) )