Metamath Proof Explorer

Theorem lmmbr

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
lmmbr.3 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
Assertion lmmbr ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 ⊒ 𝐽 = ( MetOpen β€˜ 𝐷 )
2 lmmbr.3 ⊒ ( πœ‘ β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
3 1 mopntopon ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
4 2 3 syl ⊒ ( πœ‘ β†’ 𝐽 ∈ ( TopOn β€˜ 𝑋 ) )
5 4 lmbr ⊒ ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ) )
6 rpxr ⊒ ( π‘₯ ∈ ℝ+ β†’ π‘₯ ∈ ℝ* )
7 1 blopn ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ π‘₯ ∈ ℝ* ) β†’ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∈ 𝐽 )
8 6 7 syl3an3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ π‘₯ ∈ ℝ+ ) β†’ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∈ 𝐽 )
9 blcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ π‘₯ ∈ ℝ+ ) β†’ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) )
10 eleq2 ⊒ ( 𝑒 = ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( 𝑃 ∈ 𝑒 ↔ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
11 feq3 ⊒ ( 𝑒 = ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ↔ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
12 11 rexbidv ⊒ ( 𝑒 = ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ↔ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
13 10 12 imbi12d ⊒ ( 𝑒 = ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )
14 13 rspcva ⊒ ( ( ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∈ 𝐽 ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) β†’ ( 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
15 14 impancom ⊒ ( ( ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∈ 𝐽 ∧ 𝑃 ∈ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) β†’ ( βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
16 8 9 15 syl2anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ π‘₯ ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
17 16 3expa ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ π‘₯ ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
18 17 adantlrl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ π‘₯ ∈ ℝ+ ) β†’ ( βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
19 18 impancom ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) β†’ ( π‘₯ ∈ ℝ+ β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
20 19 ralrimiv ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) β†’ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) )
21 1 mopni2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝐽 ∧ 𝑃 ∈ 𝑒 ) β†’ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 )
22 r19.29 ⊒ ( ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) β†’ βˆƒ π‘₯ ∈ ℝ+ ( βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) )
23 fss ⊒ ( ( ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) β†’ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 )
24 23 expcom ⊒ ( ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 β†’ ( ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) )
25 24 reximdv ⊒ ( ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 β†’ ( βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) )
26 25 impcom ⊒ ( ( βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 )
27 26 rexlimivw ⊒ ( βˆƒ π‘₯ ∈ ℝ+ ( βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 )
28 22 27 syl ⊒ ( ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ βˆƒ π‘₯ ∈ ℝ+ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) βŠ† 𝑒 ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 )
29 21 28 sylan2 ⊒ ( ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ∧ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑒 ∈ 𝐽 ∧ 𝑃 ∈ 𝑒 ) ) β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 )
30 29 3exp2 ⊒ ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) β†’ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝑒 ∈ 𝐽 β†’ ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ) )
31 30 impcom ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) β†’ ( 𝑒 ∈ 𝐽 β†’ ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) )
32 31 adantlr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) β†’ ( 𝑒 ∈ 𝐽 β†’ ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) )
33 32 ralrimiv ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) β†’ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) )
34 20 33 impbida ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ) β†’ ( βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
35 34 pm5.32da ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )
36 df-3an ⊒ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) )
37 df-3an ⊒ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) )
38 35 36 37 3bitr4g ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )
39 2 38 syl ⊒ ( πœ‘ β†’ ( ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ 𝑒 ∈ 𝐽 ( 𝑃 ∈ 𝑒 β†’ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ 𝑒 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )
40 5 39 bitrd ⊒ ( πœ‘ β†’ ( 𝐹 ( ⇝𝑑 β€˜ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm β„‚ ) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ ran β„€β‰₯ ( 𝐹 β†Ύ 𝑦 ) : 𝑦 ⟢ ( 𝑃 ( ball β€˜ 𝐷 ) π‘₯ ) ) ) )