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

Metamath Proof Explorer

Theorem cfilres

Description: Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cfilres ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
3 1 2 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
4 simp3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ∈ 𝐹 )
5 fbncp ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 )
6 3 4 5 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 )
7 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ⊆ 𝑋 )
8 7 3adant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ⊆ 𝑋 )
9 trfil3 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) )
10 1 8 9 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) )
11 6 10 mpbird ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) )
12 11 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) )
13 cfili ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑠 ∈ 𝐹 ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 )
14 13 adantll ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑠 ∈ 𝐹 ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 )
15 simpll2 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
16 simpll3 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑌 ∈ 𝐹 )
17 15 16 jca ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) )
18 elrestr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ∧ 𝑠 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) )
19 18 3expa ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) )
20 17 19 sylan ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝑠 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) )
21 inss1 ⊢ ( 𝑠 ∩ 𝑌 ) ⊆ 𝑠
22 ss2ralv ⊢ ( ( 𝑠 ∩ 𝑌 ) ⊆ 𝑠 → ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 → ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 𝐷 𝑣 ) < 𝑥 ) )
23 21 22 ax-mp ⊢ ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 → ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 𝐷 𝑣 ) < 𝑥 )
24 elinel2 ⊢ ( 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) → 𝑢 ∈ 𝑌 )
25 elinel2 ⊢ ( 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) → 𝑣 ∈ 𝑌 )
26 ovres ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) = ( 𝑢 𝐷 𝑣 ) )
27 26 breq1d ⊢ ( ( 𝑢 ∈ 𝑌 ∧ 𝑣 ∈ 𝑌 ) → ( ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ( 𝑢 𝐷 𝑣 ) < 𝑥 ) )
28 24 25 27 syl2an ⊢ ( ( 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∧ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ) → ( ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ( 𝑢 𝐷 𝑣 ) < 𝑥 ) )
29 28 ralbidva ⊢ ( 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) → ( ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 𝐷 𝑣 ) < 𝑥 ) )
30 29 ralbiia ⊢ ( ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 𝐷 𝑣 ) < 𝑥 )
31 23 30 sylibr ⊢ ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 → ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 )
32 raleq ⊢ ( 𝑦 = ( 𝑠 ∩ 𝑌 ) → ( ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) )
33 32 raleqbi1dv ⊢ ( 𝑦 = ( 𝑠 ∩ 𝑌 ) → ( ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ↔ ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) )
34 33 rspcev ⊢ ( ( ( 𝑠 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ∧ ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 )
35 34 ex ⊢ ( ( 𝑠 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) → ( ∀ 𝑢 ∈ ( 𝑠 ∩ 𝑌 ) ∀ 𝑣 ∈ ( 𝑠 ∩ 𝑌 ) ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) )
36 20 31 35 syl2im ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑠 ∈ 𝐹 ) → ( ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) )
37 36 rexlimdva ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑠 ∈ 𝐹 ∀ 𝑢 ∈ 𝑠 ∀ 𝑣 ∈ 𝑠 ( 𝑢 𝐷 𝑣 ) < 𝑥 → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) )
38 14 37 mpd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 )
39 38 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 )
40 simp1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
41 xmetres2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
42 40 8 41 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
43 42 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
44 iscfil2 ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) ) )
45 43 44 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ↔ ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ∀ 𝑢 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑢 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑣 ) < 𝑥 ) ) )
46 12 39 45 mpbir2and ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
47 46 ex ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
48 cfilresi ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) → ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) ∈ ( CauFil ‘ 𝐷 ) )
49 48 ex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) ∈ ( CauFil ‘ 𝐷 ) ) )
50 49 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) ∈ ( CauFil ‘ 𝐷 ) ) )
51 fgtr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) = 𝐹 )
52 51 3adant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) = 𝐹 )
53 52 eleq1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝑋 filGen ( 𝐹 ↾t 𝑌 ) ) ∈ ( CauFil ‘ 𝐷 ) ↔ 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) )
54 50 53 sylibd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) → 𝐹 ∈ ( CauFil ‘ 𝐷 ) ) )
55 47 54 impbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ↾t 𝑌 ) ∈ ( CauFil ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )