This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cfilfcls

Description: Similar to ultrafilters ( uffclsflim ), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses cfilfcls.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
cfilfcls.2 ⊢ 𝑋 = dom dom 𝐷
Assertion cfilfcls ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐽 fClus 𝐹 ) = ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 cfilfcls.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 cfilfcls.2 ⊢ 𝑋 = dom dom 𝐷
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 fclselbas ⊢ ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) → 𝑥 ∈ ∪ 𝐽 )
5 4 adantl ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑥 ∈ ∪ 𝐽 )
6 df-cfil ⊢ CauFil = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
7 6 mptrcl ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐷 ∈ ∪ ran ∞Met )
8 xmetunirn ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
9 7 8 sylib ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
10 2 fveq2i ⊢ ( ∞Met ‘ 𝑋 ) = ( ∞Met ‘ dom dom 𝐷 )
11 9 10 eleqtrrdi ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
12 11 adantr ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
13 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 12 13 syl ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
16 14 15 syl ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑋 = ∪ 𝐽 )
17 5 16 eleqtrrd ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑥 ∈ 𝑋 )
18 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
19 18 3expb ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
20 12 19 sylan ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
21 cfilfil ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
22 11 21 mpancom ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
24 23 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
25 12 adantr ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
26 simpll ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐹 ∈ ( CauFil ‘ 𝐷 ) )
27 rphalfcl ⊢ ( 𝑟 ∈ ℝ+ → ( 𝑟 / 2 ) ∈ ℝ+ )
28 27 adantl ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / 2 ) ∈ ℝ+ )
29 rphalfcl ⊢ ( ( 𝑟 / 2 ) ∈ ℝ+ → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
30 28 29 syl ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ )
31 cfil3i ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ ( ( 𝑟 / 2 ) / 2 ) ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 )
32 25 26 30 31 syl3anc ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 )
33 23 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
34 simprr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 )
35 25 adantr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
36 17 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝑥 ∈ 𝑋 )
37 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
38 37 ad2antlr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝑟 ∈ ℝ* )
39 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 )
40 35 36 38 39 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 )
41 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fClus 𝐹 ) )
42 28 adantr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
43 42 rpxrd ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑟 / 2 ) ∈ ℝ* )
44 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
45 35 36 43 44 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 )
46 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ+ ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
47 35 36 42 46 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
48 fclsopni ⊢ ( ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∈ 𝐽 ∧ 𝑥 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ≠ ∅ )
49 41 45 47 34 48 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ≠ ∅ )
50 n0 ⊢ ( ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) )
51 49 50 sylib ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ∃ 𝑧 𝑧 ∈ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) )
52 elin ⊢ ( 𝑧 ∈ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ↔ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) )
53 35 adantr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
54 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑦 ∈ 𝑋 )
55 42 adantr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ+ )
56 55 rpred ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ )
57 simprr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) )
58 blhalf ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) ∧ ( ( 𝑟 / 2 ) ∈ ℝ ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
59 53 54 56 57 58 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
60 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑟 / 2 ) ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ 𝑋 )
61 35 36 43 60 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ 𝑋 )
62 61 sselda ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) → 𝑧 ∈ 𝑋 )
63 62 adantrr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑧 ∈ 𝑋 )
64 simpllr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑟 ∈ ℝ+ )
65 64 rpred ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑟 ∈ ℝ )
66 simprl ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
67 55 rpxrd ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑟 / 2 ) ∈ ℝ* )
68 36 adantr ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑥 ∈ 𝑋 )
69 blcom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑟 / 2 ) ∈ ℝ* ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ 𝑥 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
70 53 67 68 63 69 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ↔ 𝑥 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) )
71 66 70 mpbid ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → 𝑥 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) )
72 blhalf ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑟 ∈ ℝ ∧ 𝑥 ∈ ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ) ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
73 53 63 65 71 72 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
74 59 73 sstrd ⊢ ( ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) ∧ ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
75 74 ex ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( ( 𝑧 ∈ ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∧ 𝑧 ∈ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
76 52 75 biimtrid ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑧 ∈ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
77 76 exlimdv ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( ∃ 𝑧 𝑧 ∈ ( ( 𝑥 ( ball ‘ 𝐷 ) ( 𝑟 / 2 ) ) ∩ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) )
78 51 77 mpd ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) )
79 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ⊆ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 )
80 33 34 40 78 79 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝑦 ( ball ‘ 𝐷 ) ( ( 𝑟 / 2 ) / 2 ) ) ∈ 𝐹 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 )
81 32 80 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 )
82 81 ad2ant2r ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 )
83 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ⊆ 𝑋 )
84 83 adantrr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
85 14 84 sylan ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
86 85 adantr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ⊆ 𝑋 )
87 simprr ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
88 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
89 24 82 86 87 88 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝑥 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
90 20 89 rexlimddv ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
91 90 expr ⊢ ( ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
92 91 ralrimiva ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) )
93 flimopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
94 14 23 93 syl2anc ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
95 17 92 94 mpbir2and ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ( 𝐽 fClus 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
96 95 ex ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝐹 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
97 96 ssrdv ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐽 fClus 𝐹 ) ⊆ ( 𝐽 fLim 𝐹 ) )
98 flimfcls ⊢ ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 )
99 98 a1i ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐽 fLim 𝐹 ) ⊆ ( 𝐽 fClus 𝐹 ) )
100 97 99 eqssd ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐽 fClus 𝐹 ) = ( 𝐽 fLim 𝐹 ) )