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 F Fil X G Fil X F G Fil X

Proof

Step Hyp Ref Expression
1 inss1 F G F
2 filsspw F Fil X F 𝒫 X
3 2 adantr F Fil X G Fil X F 𝒫 X
4 1 3 sstrid F Fil X G Fil X F G 𝒫 X
5 0nelfil F Fil X ¬ F
6 5 adantr F Fil X G Fil X ¬ F
7 elinel1 F G F
8 6 7 nsyl F Fil X G Fil X ¬ F G
9 filtop F Fil X X F
10 9 adantr F Fil X G Fil X X F
11 filtop G Fil X X G
12 11 adantl F Fil X G Fil X X G
13 10 12 elind F Fil X G Fil X X F G
14 4 8 13 3jca F Fil X G Fil X F G 𝒫 X ¬ F G X F G
15 simpll F Fil X G Fil X x 𝒫 X y F G y x F Fil X
16 simpr2 F Fil X G Fil X x 𝒫 X y F G y x y F G
17 elinel1 y F G y F
18 16 17 syl F Fil X G Fil X x 𝒫 X y F G y x y F
19 simpr1 F Fil X G Fil X x 𝒫 X y F G y x x 𝒫 X
20 19 elpwid F Fil X G Fil X x 𝒫 X y F G y x x X
21 simpr3 F Fil X G Fil X x 𝒫 X y F G y x y x
22 filss F Fil X y F x X y x x F
23 15 18 20 21 22 syl13anc F Fil X G Fil X x 𝒫 X y F G y x x F
24 simplr F Fil X G Fil X x 𝒫 X y F G y x G Fil X
25 elinel2 y F G y G
26 16 25 syl F Fil X G Fil X x 𝒫 X y F G y x y G
27 filss G Fil X y G x X y x x G
28 24 26 20 21 27 syl13anc F Fil X G Fil X x 𝒫 X y F G y x x G
29 23 28 elind F Fil X G Fil X x 𝒫 X y F G y x x F G
30 29 3exp2 F Fil X G Fil X x 𝒫 X y F G y x x F G
31 30 imp F Fil X G Fil X x 𝒫 X y F G y x x F G
32 31 rexlimdv F Fil X G Fil X x 𝒫 X y F G y x x F G
33 32 ralrimiva F Fil X G Fil X x 𝒫 X y F G y x x F G
34 simpl F Fil X G Fil X F Fil X
35 elinel1 x F G x F
36 35 17 anim12i x F G y F G x F y F
37 filin F Fil X x F y F x y F
38 37 3expb F Fil X x F y F x y F
39 34 36 38 syl2an F Fil X G Fil X x F G y F G x y F
40 simpr F Fil X G Fil X G Fil X
41 elinel2 x F G x G
42 41 25 anim12i x F G y F G x G y G
43 filin G Fil X x G y G x y G
44 43 3expb G Fil X x G y G x y G
45 40 42 44 syl2an F Fil X G Fil X x F G y F G x y G
46 39 45 elind F Fil X G Fil X x F G y F G x y F G
47 46 ralrimivva F Fil X G Fil X x F G y F G x y F G
48 isfil2 F G Fil X F G 𝒫 X ¬ F G X F G x 𝒫 X y F G y x x F G x F G y F G x y F G
49 14 33 47 48 syl3anbrc F Fil X G Fil X F G Fil X