Metamath Proof Explorer


Theorem cfilresi

Description: A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cfilresi ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( 𝑋 filGen 𝐹 ) ∈ ( CauFil β€˜ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 xmetres ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) )
2 iscfil2 ⊒ ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) β†’ ( 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ↔ ( 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) ∧ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ ) ) )
3 2 simplbda ⊒ ( ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ )
4 1 3 sylan ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ )
5 cfilfil ⊒ ( ( ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ∈ ( ∞Met β€˜ ( 𝑋 ∩ π‘Œ ) ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) )
6 1 5 sylan ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) )
7 filelss ⊒ ( ( 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) ∧ 𝑦 ∈ 𝐹 ) β†’ 𝑦 βŠ† ( 𝑋 ∩ π‘Œ ) )
8 6 7 sylan ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) β†’ 𝑦 βŠ† ( 𝑋 ∩ π‘Œ ) )
9 inss2 ⊒ ( 𝑋 ∩ π‘Œ ) βŠ† π‘Œ
10 8 9 sstrdi ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) β†’ 𝑦 βŠ† π‘Œ )
11 10 sselda ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) ∧ 𝑒 ∈ 𝑦 ) β†’ 𝑒 ∈ π‘Œ )
12 10 sselda ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) ∧ 𝑣 ∈ 𝑦 ) β†’ 𝑣 ∈ π‘Œ )
13 11 12 anim12dan ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑒 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦 ) ) β†’ ( 𝑒 ∈ π‘Œ ∧ 𝑣 ∈ π‘Œ ) )
14 ovres ⊒ ( ( 𝑒 ∈ π‘Œ ∧ 𝑣 ∈ π‘Œ ) β†’ ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) = ( 𝑒 𝐷 𝑣 ) )
15 13 14 syl ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑒 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦 ) ) β†’ ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) = ( 𝑒 𝐷 𝑣 ) )
16 15 breq1d ⊒ ( ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑒 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦 ) ) β†’ ( ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ ↔ ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
17 16 2ralbidva ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) ∧ 𝑦 ∈ 𝐹 ) β†’ ( βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ ↔ βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
18 17 rexbidva ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ ↔ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
19 18 ralbidv ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) 𝑣 ) < π‘₯ ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
20 4 19 mpbid ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ )
21 filfbas ⊒ ( 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) β†’ 𝐹 ∈ ( fBas β€˜ ( 𝑋 ∩ π‘Œ ) ) )
22 6 21 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 ∈ ( fBas β€˜ ( 𝑋 ∩ π‘Œ ) ) )
23 filsspw ⊒ ( 𝐹 ∈ ( Fil β€˜ ( 𝑋 ∩ π‘Œ ) ) β†’ 𝐹 βŠ† 𝒫 ( 𝑋 ∩ π‘Œ ) )
24 6 23 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 βŠ† 𝒫 ( 𝑋 ∩ π‘Œ ) )
25 inss1 ⊒ ( 𝑋 ∩ π‘Œ ) βŠ† 𝑋
26 25 sspwi ⊒ 𝒫 ( 𝑋 ∩ π‘Œ ) βŠ† 𝒫 𝑋
27 24 26 sstrdi ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 βŠ† 𝒫 𝑋 )
28 elfvdm ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 ∈ dom ∞Met )
29 28 adantr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝑋 ∈ dom ∞Met )
30 fbasweak ⊒ ( ( 𝐹 ∈ ( fBas β€˜ ( 𝑋 ∩ π‘Œ ) ) ∧ 𝐹 βŠ† 𝒫 𝑋 ∧ 𝑋 ∈ dom ∞Met ) β†’ 𝐹 ∈ ( fBas β€˜ 𝑋 ) )
31 22 27 29 30 syl3anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ 𝐹 ∈ ( fBas β€˜ 𝑋 ) )
32 fgcfil ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( fBas β€˜ 𝑋 ) ) β†’ ( ( 𝑋 filGen 𝐹 ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
33 31 32 syldan ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( ( 𝑋 filGen 𝐹 ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐹 βˆ€ 𝑒 ∈ 𝑦 βˆ€ 𝑣 ∈ 𝑦 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
34 20 33 mpbird ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐹 ∈ ( CauFil β€˜ ( 𝐷 β†Ύ ( π‘Œ Γ— π‘Œ ) ) ) ) β†’ ( 𝑋 filGen 𝐹 ) ∈ ( CauFil β€˜ 𝐷 ) )