| 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 ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ) |