Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  infil Unicode version

Theorem infil 17844
 Description: The intersection of two filters is a filter. Use fiint 7340 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.)
Assertion
Ref Expression
infil

Proof of Theorem infil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3519 . . . 4
2 filsspw 17832 . . . . 5
32adantr 452 . . . 4
41, 3syl5ss 3317 . . 3
5 0nelfil 17830 . . . . 5
65adantr 452 . . . 4
71sseli 3302 . . . 4
86, 7nsyl 115 . . 3
9 filtop 17836 . . . . 5
109adantr 452 . . . 4
11 filtop 17836 . . . . 5
1211adantl 453 . . . 4
13 elin 3488 . . . 4
1410, 12, 13sylanbrc 646 . . 3
154, 8, 143jca 1134 . 2
16 simpll 731 . . . . . . . 8
17 simpr2 964 . . . . . . . . 9
181sseli 3302 . . . . . . . . 9
1917, 18syl 16 . . . . . . . 8
20 simpr1 963 . . . . . . . . 9
2120elpwid 3766 . . . . . . . 8
22 simpr3 965 . . . . . . . 8
23 filss 17834 . . . . . . . 8
2416, 19, 21, 22, 23syl13anc 1186 . . . . . . 7
25 simplr 732 . . . . . . . 8
26 inss2 3520 . . . . . . . . . 10
2726sseli 3302 . . . . . . . . 9
2817, 27syl 16 . . . . . . . 8
29 filss 17834 . . . . . . . 8
3025, 28, 21, 22, 29syl13anc 1186 . . . . . . 7
31 elin 3488 . . . . . . 7
3224, 30, 31sylanbrc 646 . . . . . 6
33323exp2 1171 . . . . 5
3433imp 419 . . . 4
3534rexlimdv 2787 . . 3
3635ralrimiva 2747 . 2
37 simpl 444 . . . . 5
381sseli 3302 . . . . . 6
3938, 18anim12i 550 . . . . 5
40 filin 17835 . . . . . 6
41403expb 1154 . . . . 5
4237, 39, 41syl2an 464 . . . 4
43 simpr 448 . . . . 5
4426sseli 3302 . . . . . 6
4544, 27anim12i 550 . . . . 5
46 filin 17835 . . . . . 6
47463expb 1154 . . . . 5
4843, 45, 47syl2an 464 . . . 4
49 elin 3488 . . . 4
5042, 48, 49sylanbrc 646 . . 3
5150ralrimivva 2756 . 2
52 isfil2 17837 . 2
5315, 36, 51, 52syl3anbrc 1138 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   w3a 936   wcel 1721  wral 2664  wrex 2665   cin 3277   wss 3278  c0 3586  cpw 3757  cfv 5411  cfil 17826 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2383  ax-sep 4288  ax-nul 4296  ax-pow 4335  ax-pr 4361 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2389  df-cleq 2395  df-clel 2398  df-nfc 2527  df-ne 2567  df-nel 2568  df-ral 2669  df-rex 2670  df-rab 2673  df-v 2916  df-sbc 3120  df-csb 3210  df-dif 3281  df-un 3283  df-in 3285  df-ss 3292  df-nul 3587  df-if 3698  df-pw 3759  df-sn 3778  df-pr 3779  df-op 3781  df-uni 3974  df-br 4171  df-opab 4225  df-mpt 4226  df-id 4456  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5375  df-fun 5413  df-fv 5419  df-fbas 16650  df-fil 17827
 Copyright terms: Public domain W3C validator