Description: The intersection of two filters is a filter. Use fiint to extend this property to the intersection of a finite set of filters. Paragraph 3 of BourbakiTop1 p. I.36. (Contributed by FL, 17-Sep-2007) (Revised by Stefan O'Rear, 2-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | infil | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 | |
|
2 | filsspw | |
|
3 | 2 | adantr | |
4 | 1 3 | sstrid | |
5 | 0nelfil | |
|
6 | 5 | adantr | |
7 | elinel1 | |
|
8 | 6 7 | nsyl | |
9 | filtop | |
|
10 | 9 | adantr | |
11 | filtop | |
|
12 | 11 | adantl | |
13 | 10 12 | elind | |
14 | 4 8 13 | 3jca | |
15 | simpll | |
|
16 | simpr2 | |
|
17 | elinel1 | |
|
18 | 16 17 | syl | |
19 | simpr1 | |
|
20 | 19 | elpwid | |
21 | simpr3 | |
|
22 | filss | |
|
23 | 15 18 20 21 22 | syl13anc | |
24 | simplr | |
|
25 | elinel2 | |
|
26 | 16 25 | syl | |
27 | filss | |
|
28 | 24 26 20 21 27 | syl13anc | |
29 | 23 28 | elind | |
30 | 29 | 3exp2 | |
31 | 30 | imp | |
32 | 31 | rexlimdv | |
33 | 32 | ralrimiva | |
34 | simpl | |
|
35 | elinel1 | |
|
36 | 35 17 | anim12i | |
37 | filin | |
|
38 | 37 | 3expb | |
39 | 34 36 38 | syl2an | |
40 | simpr | |
|
41 | elinel2 | |
|
42 | 41 25 | anim12i | |
43 | filin | |
|
44 | 43 | 3expb | |
45 | 40 42 44 | syl2an | |
46 | 39 45 | elind | |
47 | 46 | ralrimivva | |
48 | isfil2 | |
|
49 | 14 33 47 48 | syl3anbrc | |