Metamath Proof Explorer


Theorem cfil3i

Description: A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cfil3i ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ βˆƒ π‘₯ ∈ 𝑋 ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 cfili ⊒ ( ( 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ βˆƒ 𝑠 ∈ 𝐹 βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 )
2 1 3adant1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ βˆƒ 𝑠 ∈ 𝐹 βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 )
3 cfilfil ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ) β†’ 𝐹 ∈ ( Fil β€˜ 𝑋 ) )
4 3 3adant3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ 𝐹 ∈ ( Fil β€˜ 𝑋 ) )
5 fileln0 ⊒ ( ( 𝐹 ∈ ( Fil β€˜ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) β†’ 𝑠 β‰  βˆ… )
6 4 5 sylan ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ 𝑠 β‰  βˆ… )
7 r19.2z ⊒ ( ( 𝑠 β‰  βˆ… ∧ βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) β†’ βˆƒ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 )
8 7 ex ⊒ ( 𝑠 β‰  βˆ… β†’ ( βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
9 6 8 syl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ ( βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
10 filelss ⊒ ( ( 𝐹 ∈ ( Fil β€˜ 𝑋 ) ∧ 𝑠 ∈ 𝐹 ) β†’ 𝑠 βŠ† 𝑋 )
11 4 10 sylan ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ 𝑠 βŠ† 𝑋 )
12 ssrexv ⊒ ( 𝑠 βŠ† 𝑋 β†’ ( βˆƒ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
13 11 12 syl ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ ( βˆƒ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
14 dfss3 ⊒ ( 𝑠 βŠ† ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ↔ βˆ€ 𝑦 ∈ 𝑠 𝑦 ∈ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) )
15 simpl1 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
16 15 ad2antrr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
17 simpll3 ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 ∈ ℝ+ )
18 17 rpxrd ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑅 ∈ ℝ* )
19 18 adantr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) β†’ 𝑅 ∈ ℝ* )
20 simplr ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) β†’ π‘₯ ∈ 𝑋 )
21 11 adantr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑠 βŠ† 𝑋 )
22 21 sselda ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) β†’ 𝑦 ∈ 𝑋 )
23 elbl2 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( π‘₯ ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) β†’ ( 𝑦 ∈ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ↔ ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
24 16 19 20 22 23 syl22anc ⊒ ( ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑠 ) β†’ ( 𝑦 ∈ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ↔ ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
25 24 ralbidva ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( βˆ€ 𝑦 ∈ 𝑠 𝑦 ∈ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ↔ βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
26 14 25 bitrid ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑠 βŠ† ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ↔ βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 ) )
27 4 ad2antrr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝐹 ∈ ( Fil β€˜ 𝑋 ) )
28 simplr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝑠 ∈ 𝐹 )
29 15 adantr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
30 simpr ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ π‘₯ ∈ 𝑋 )
31 blssm ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ π‘₯ ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† 𝑋 )
32 29 30 18 31 syl3anc ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† 𝑋 )
33 filss ⊒ ( ( 𝐹 ∈ ( Fil β€˜ 𝑋 ) ∧ ( 𝑠 ∈ 𝐹 ∧ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† 𝑋 ∧ 𝑠 βŠ† ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ) ) β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 )
34 33 3exp2 ⊒ ( 𝐹 ∈ ( Fil β€˜ 𝑋 ) β†’ ( 𝑠 ∈ 𝐹 β†’ ( ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† 𝑋 β†’ ( 𝑠 βŠ† ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) ) ) )
35 27 28 32 34 syl3c ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( 𝑠 βŠ† ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
36 26 35 sylbird ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) ∧ π‘₯ ∈ 𝑋 ) β†’ ( βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
37 36 reximdva ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ ( βˆƒ π‘₯ ∈ 𝑋 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑋 ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
38 9 13 37 3syld ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) β†’ ( βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑋 ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
39 38 rexlimdva ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ ( βˆƒ 𝑠 ∈ 𝐹 βˆ€ π‘₯ ∈ 𝑠 βˆ€ 𝑦 ∈ 𝑠 ( π‘₯ 𝐷 𝑦 ) < 𝑅 β†’ βˆƒ π‘₯ ∈ 𝑋 ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 ) )
40 2 39 mpd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) β†’ βˆƒ π‘₯ ∈ 𝑋 ( π‘₯ ( ball β€˜ 𝐷 ) 𝑅 ) ∈ 𝐹 )