Description: A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fbssint | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fbasne0 | |
|
2 | n0 | |
|
3 | 1 2 | sylib | |
4 | ssv | |
|
5 | 4 | jctr | |
6 | 5 | eximi | |
7 | df-rex | |
|
8 | 6 7 | sylibr | |
9 | 3 8 | syl | |
10 | inteq | |
|
11 | int0 | |
|
12 | 10 11 | eqtrdi | |
13 | 12 | sseq2d | |
14 | 13 | rexbidv | |
15 | 9 14 | syl5ibrcom | |
16 | 15 | 3ad2ant1 | |
17 | simpl1 | |
|
18 | simpl2 | |
|
19 | simpr | |
|
20 | simpl3 | |
|
21 | elfir | |
|
22 | 17 18 19 20 21 | syl13anc | |
23 | fbssfi | |
|
24 | 17 22 23 | syl2anc | |
25 | 24 | ex | |
26 | 16 25 | pm2.61dne | |