Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
2 |
|
filelss |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ⊆ 𝑋 ) |
3 |
2
|
3adant1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ⊆ 𝑋 ) |
4 |
|
resttopon |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ) |
5 |
1 3 4
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ) |
6 |
|
filfbas |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) ) |
8 |
|
simp3 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝑌 ∈ 𝐹 ) |
9 |
|
fbncp |
⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) |
10 |
7 8 9
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) |
11 |
|
simp2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
12 |
|
trfil3 |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) ) |
13 |
11 3 12
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ↔ ¬ ( 𝑋 ∖ 𝑌 ) ∈ 𝐹 ) ) |
14 |
10 13
|
mpbird |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ) |
15 |
|
flimopn |
⊢ ( ( ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐹 ↾t 𝑌 ) ∈ ( Fil ‘ 𝑌 ) ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) ) |
16 |
5 14 15
|
syl2anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) ) |
17 |
|
simpll2 |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
18 |
|
simpll3 |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑌 ∈ 𝐹 ) |
19 |
|
elrestr |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) |
20 |
19
|
3expia |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑧 ∈ 𝐹 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) |
21 |
17 18 20
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∈ 𝐹 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) |
22 |
|
trfilss |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝐹 ↾t 𝑌 ) ⊆ 𝐹 ) |
23 |
17 18 22
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐹 ↾t 𝑌 ) ⊆ 𝐹 ) |
24 |
23
|
sseld |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) → ( 𝑧 ∩ 𝑌 ) ∈ 𝐹 ) ) |
25 |
|
inss1 |
⊢ ( 𝑧 ∩ 𝑌 ) ⊆ 𝑧 |
26 |
25
|
a1i |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∩ 𝑌 ) ⊆ 𝑧 ) |
27 |
|
simpl1 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
28 |
|
toponss |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ⊆ 𝑋 ) |
29 |
27 28
|
sylan |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ⊆ 𝑋 ) |
30 |
|
filss |
⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑧 ∩ 𝑌 ) ∈ 𝐹 ∧ 𝑧 ⊆ 𝑋 ∧ ( 𝑧 ∩ 𝑌 ) ⊆ 𝑧 ) ) → 𝑧 ∈ 𝐹 ) |
31 |
30
|
3exp2 |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑧 ∩ 𝑌 ) ∈ 𝐹 → ( 𝑧 ⊆ 𝑋 → ( ( 𝑧 ∩ 𝑌 ) ⊆ 𝑧 → 𝑧 ∈ 𝐹 ) ) ) ) |
32 |
31
|
com24 |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑧 ∩ 𝑌 ) ⊆ 𝑧 → ( 𝑧 ⊆ 𝑋 → ( ( 𝑧 ∩ 𝑌 ) ∈ 𝐹 → 𝑧 ∈ 𝐹 ) ) ) ) |
33 |
17 26 29 32
|
syl3c |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑧 ∩ 𝑌 ) ∈ 𝐹 → 𝑧 ∈ 𝐹 ) ) |
34 |
24 33
|
syld |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) → 𝑧 ∈ 𝐹 ) ) |
35 |
21 34
|
impbid |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∈ 𝐹 ↔ ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) |
36 |
35
|
imbi2d |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ↔ ( 𝑥 ∈ 𝑧 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) |
37 |
36
|
ralbidva |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) |
38 |
|
simpl2 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
39 |
3
|
sselda |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 ) |
40 |
|
flimopn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) ) ) |
41 |
40
|
baibd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) ) |
42 |
27 38 39 41
|
syl21anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹 ) ) ) |
43 |
|
vex |
⊢ 𝑧 ∈ V |
44 |
43
|
inex1 |
⊢ ( 𝑧 ∩ 𝑌 ) ∈ V |
45 |
44
|
a1i |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝑧 ∩ 𝑌 ) ∈ V ) |
46 |
|
simpl3 |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑌 ∈ 𝐹 ) |
47 |
|
elrest |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑧 ∈ 𝐽 𝑦 = ( 𝑧 ∩ 𝑌 ) ) ) |
48 |
27 46 47
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ↔ ∃ 𝑧 ∈ 𝐽 𝑦 = ( 𝑧 ∩ 𝑌 ) ) ) |
49 |
|
eleq2 |
⊢ ( 𝑦 = ( 𝑧 ∩ 𝑌 ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ( 𝑧 ∩ 𝑌 ) ) ) |
50 |
|
elin |
⊢ ( 𝑥 ∈ ( 𝑧 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑌 ) ) |
51 |
50
|
rbaib |
⊢ ( 𝑥 ∈ 𝑌 → ( 𝑥 ∈ ( 𝑧 ∩ 𝑌 ) ↔ 𝑥 ∈ 𝑧 ) ) |
52 |
51
|
adantl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝑧 ∩ 𝑌 ) ↔ 𝑥 ∈ 𝑧 ) ) |
53 |
49 52
|
sylan9bbr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑧 ∩ 𝑌 ) ) → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) ) |
54 |
|
eleq1 |
⊢ ( 𝑦 = ( 𝑧 ∩ 𝑌 ) → ( 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ↔ ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) |
55 |
54
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑧 ∩ 𝑌 ) ) → ( 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ↔ ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) |
56 |
53 55
|
imbi12d |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 = ( 𝑧 ∩ 𝑌 ) ) → ( ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑧 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) |
57 |
45 48 56
|
ralxfr2d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 → ( 𝑧 ∩ 𝑌 ) ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) |
58 |
37 42 57
|
3bitr4d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) |
59 |
58
|
pm5.32da |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ∀ 𝑦 ∈ ( 𝐽 ↾t 𝑌 ) ( 𝑥 ∈ 𝑦 → 𝑦 ∈ ( 𝐹 ↾t 𝑌 ) ) ) ) ) |
60 |
16 59
|
bitr4d |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝐹 ↾t 𝑌 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ) ) |
61 |
|
ancom |
⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ) |
62 |
|
elin |
⊢ ( 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑥 ∈ 𝑌 ) ) |
63 |
61 62
|
bitr4i |
⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) ↔ 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ) |
64 |
60 63
|
bitrdi |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝐹 ↾t 𝑌 ) ) ↔ 𝑥 ∈ ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ) ) |
65 |
64
|
eqrdv |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑌 ∈ 𝐹 ) → ( ( 𝐽 ↾t 𝑌 ) fLim ( 𝐹 ↾t 𝑌 ) ) = ( ( 𝐽 fLim 𝐹 ) ∩ 𝑌 ) ) |