Theorem filfbas 20217

Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.)

Assertion

Ref	Expression
filfbas	|- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )

Proof of Theorem filfbas

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfil 20216	. 2 |- ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
2	1	simplbi 460	1 |- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )

Syntax hints:   -> wi 4   e. wcel 1767   =/= wne 2662   A.wral 2817   i^i cin 3480   (/)c0 3790   ~Pcpw 4016   ` cfv 5594   fBascfbas 18276   Filcfil 20214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-fil 20215

This theorem is referenced by:  0nelfil  20218  filsspw  20220  filelss  20221  filin  20223  filtop  20224  snfbas  20235  fgfil  20244  elfilss  20245  filfinnfr  20246  fgabs  20248  filcon  20252  fgtr  20259  trfg  20260  ufilb  20275  ufilmax  20276  isufil2  20277  ssufl  20287  ufileu  20288  filufint  20289  ufilen  20299  fmfg  20318  fmufil  20328  fmid  20329  fmco  20330  ufldom  20331  hausflim  20350  flimrest  20352  flimclslem  20353  flfnei  20360  isflf  20362  flfcnp  20373  fclsrest  20393  fclsfnflim  20396  flimfnfcls  20397  isfcf  20403  cnpfcfi  20409  cnpfcf  20410  cnextcn  20435  cfilufg  20664  neipcfilu  20667  cnextucn  20674  ucnextcn  20675  cfilresi  21602  cfilres  21603  cmetss  21621  relcmpcmet  21623  cfilucfil3OLD  21625  cfilucfil3  21626  minveclem4a  21713  filnetlem4  30126