Theorem filfbas 19263

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 19262	. 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 457	1 |- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )

Syntax hints:   -> wi 4   e. wcel 1755   =/= wne 2596   A.wral 2705   i^i cin 3315   (/)c0 3625   ~Pcpw 3848   ` cfv 5406   fBascfbas 17648   Filcfil 19260

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fv 5414  df-fil 19261

This theorem is referenced by:  0nelfil  19264  filsspw  19266  filelss  19267  filin  19269  filtop  19270  snfbas  19281  fgfil  19290  elfilss  19291  filfinnfr  19292  fgabs  19294  filcon  19298  fgtr  19305  trfg  19306  ufilb  19321  ufilmax  19322  isufil2  19323  ssufl  19333  ufileu  19334  filufint  19335  ufilen  19345  fmfg  19364  fmufil  19374  fmid  19375  fmco  19376  ufldom  19377  hausflim  19396  flimrest  19398  flimclslem  19399  flfnei  19406  isflf  19408  flfcnp  19419  fclsrest  19439  fclsfnflim  19442  flimfnfcls  19443  isfcf  19449  cnpfcfi  19455  cnpfcf  19456  cnextcn  19481  cfilufg  19710  neipcfilu  19713  cnextucn  19720  ucnextcn  19721  cfilresi  20648  cfilres  20649  cmetss  20667  relcmpcmet  20669  cfilucfil3OLD  20671  cfilucfil3  20672  minveclem4a  20759  filnetlem4  28446