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 𝐹 ) )