Metamath Proof Explorer


Theorem infil

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 FFilXGFilXFGFilX

Proof

Step Hyp Ref Expression
1 inss1 FGF
2 filsspw FFilXF𝒫X
3 2 adantr FFilXGFilXF𝒫X
4 1 3 sstrid FFilXGFilXFG𝒫X
5 0nelfil FFilX¬F
6 5 adantr FFilXGFilX¬F
7 elinel1 FGF
8 6 7 nsyl FFilXGFilX¬FG
9 filtop FFilXXF
10 9 adantr FFilXGFilXXF
11 filtop GFilXXG
12 11 adantl FFilXGFilXXG
13 10 12 elind FFilXGFilXXFG
14 4 8 13 3jca FFilXGFilXFG𝒫X¬FGXFG
15 simpll FFilXGFilXx𝒫XyFGyxFFilX
16 simpr2 FFilXGFilXx𝒫XyFGyxyFG
17 elinel1 yFGyF
18 16 17 syl FFilXGFilXx𝒫XyFGyxyF
19 simpr1 FFilXGFilXx𝒫XyFGyxx𝒫X
20 19 elpwid FFilXGFilXx𝒫XyFGyxxX
21 simpr3 FFilXGFilXx𝒫XyFGyxyx
22 filss FFilXyFxXyxxF
23 15 18 20 21 22 syl13anc FFilXGFilXx𝒫XyFGyxxF
24 simplr FFilXGFilXx𝒫XyFGyxGFilX
25 elinel2 yFGyG
26 16 25 syl FFilXGFilXx𝒫XyFGyxyG
27 filss GFilXyGxXyxxG
28 24 26 20 21 27 syl13anc FFilXGFilXx𝒫XyFGyxxG
29 23 28 elind FFilXGFilXx𝒫XyFGyxxFG
30 29 3exp2 FFilXGFilXx𝒫XyFGyxxFG
31 30 imp FFilXGFilXx𝒫XyFGyxxFG
32 31 rexlimdv FFilXGFilXx𝒫XyFGyxxFG
33 32 ralrimiva FFilXGFilXx𝒫XyFGyxxFG
34 simpl FFilXGFilXFFilX
35 elinel1 xFGxF
36 35 17 anim12i xFGyFGxFyF
37 filin FFilXxFyFxyF
38 37 3expb FFilXxFyFxyF
39 34 36 38 syl2an FFilXGFilXxFGyFGxyF
40 simpr FFilXGFilXGFilX
41 elinel2 xFGxG
42 41 25 anim12i xFGyFGxGyG
43 filin GFilXxGyGxyG
44 43 3expb GFilXxGyGxyG
45 40 42 44 syl2an FFilXGFilXxFGyFGxyG
46 39 45 elind FFilXGFilXxFGyFGxyFG
47 46 ralrimivva FFilXGFilXxFGyFGxyFG
48 isfil2 FGFilXFG𝒫X¬FGXFGx𝒫XyFGyxxFGxFGyFGxyFG
49 14 33 47 48 syl3anbrc FFilXGFilXFGFilX