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

Theorem filin 18901
Description: A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
Assertion
Ref Expression
filin

Proof of Theorem filin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 filfbas 18895 . . 3
2 fbasssin 18883 . . 3
31, 2syl3an1 1225 . 2
4 inss1 3606 . . . . 5
5 filelss 18899 . . . . 5
64, 5syl5ss 3404 . . . 4
7 filss 18900 . . . . . . . 8
873exp2 1179 . . . . . . 7
98com23 75 . . . . . 6
109imp 420 . . . . 5
1110rexlimdv 2883 . . . 4
126, 11syldan 458 . . 3
13123adant3 982 . 2
143, 13mpd 15 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  /\w3a 939  e.wcel 1732  E.wrex 2760  i^icin 3364  C_wss 3365  `cfv 5438   cfbas 17314   cfil 18892
This theorem is referenced by:  isfil2  18903  filfi  18906  filinn0  18907  infil  18910  filcon  18930  filuni  18932  trfil2  18934  trfilss  18936  ufprim  18956  filufint  18967  rnelfmlem  18999  rnelfm  19000  fmfnfmlem2  19002  fmfnfmlem3  19003  fmfnfmlem4  19004  fmfnfm  19005  txflf  19053  fclsrest  19071  metustOLD  19612  metust  19613  filnetlem3  27781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-mpt 4378  df-id 4657  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fv 5446  df-fbas 17324  df-fil 18893
  Copyright terms: Public domain W3C validator