Theorem filfbas 23745

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 23744	. 2 ⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)))
2	1	simplbi 497	1 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2935  ∀wral 3056   ∩ cin 3943  ∅c0 4318  𝒫 cpw 4598  ‘cfv 6542  fBascfbas 21260  Filcfil 23742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-fil 23743

This theorem is referenced by:  0nelfil  23746  filsspw  23748  filelss  23749  filin  23751  filtop  23752  snfbas  23763  fgfil  23772  elfilss  23773  filfinnfr  23774  fgabs  23776  filconn  23780  fgtr  23787  trfg  23788  ufilb  23803  ufilmax  23804  isufil2  23805  ssufl  23815  ufileu  23816  filufint  23817  ufilen  23827  fmfg  23846  fmufil  23856  fmid  23857  fmco  23858  ufldom  23859  hausflim  23878  flimrest  23880  flimclslem  23881  flfnei  23888  isflf  23890  flfcnp  23901  fclsrest  23921  fclsfnflim  23924  flimfnfcls  23925  isfcf  23931  cnpfcfi  23937  cnpfcf  23938  cnextcn  23964  cfilufg  24191  neipcfilu  24194  cnextucn  24201  ucnextcn  24202  cfilresi  25216  cfilres  25217  cmetss  25237  relcmpcmet  25239  cfilucfil3  25241  minveclem4a  25351  filnetlem4  35855