Theorem filfbas 23790

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	⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))

Proof of Theorem filfbas

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfil 23789	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)))
2	1	simplbi 497	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049   ∩ cin 3898  ∅c0 4283  𝒫 cpw 4552  ‘cfv 6490  fBascfbas 21295  Filcfil 23787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fv 6498  df-fil 23788

This theorem is referenced by:  0nelfil  23791  filsspw  23793  filelss  23794  filin  23796  filtop  23797  snfbas  23808  fgfil  23817  elfilss  23818  filfinnfr  23819  fgabs  23821  filconn  23825  fgtr  23832  trfg  23833  ufilb  23848  ufilmax  23849  isufil2  23850  ssufl  23860  ufileu  23861  filufint  23862  ufilen  23872  fmfg  23891  fmufil  23901  fmid  23902  fmco  23903  ufldom  23904  hausflim  23923  flimrest  23925  flimclslem  23926  flfnei  23933  isflf  23935  flfcnp  23946  fclsrest  23966  fclsfnflim  23969  flimfnfcls  23970  isfcf  23976  cnpfcfi  23982  cnpfcf  23983  cnextcn  24009  cfilufg  24234  neipcfilu  24237  cnextucn  24244  ucnextcn  24245  cfilresi  25249  cfilres  25250  cmetss  25270  relcmpcmet  25272  cfilucfil3  25274  minveclem4a  25384  filnetlem4  36524