Theorem filfbas 23733

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044   ∩ cin 3902  ∅c0 4284  𝒫 cpw 4551  ‘cfv 6482  fBascfbas 21249  Filcfil 23730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fv 6490  df-fil 23731

This theorem is referenced by:  0nelfil  23734  filsspw  23736  filelss  23737  filin  23739  filtop  23740  snfbas  23751  fgfil  23760  elfilss  23761  filfinnfr  23762  fgabs  23764  filconn  23768  fgtr  23775  trfg  23776  ufilb  23791  ufilmax  23792  isufil2  23793  ssufl  23803  ufileu  23804  filufint  23805  ufilen  23815  fmfg  23834  fmufil  23844  fmid  23845  fmco  23846  ufldom  23847  hausflim  23866  flimrest  23868  flimclslem  23869  flfnei  23876  isflf  23878  flfcnp  23889  fclsrest  23909  fclsfnflim  23912  flimfnfcls  23913  isfcf  23919  cnpfcfi  23925  cnpfcf  23926  cnextcn  23952  cfilufg  24178  neipcfilu  24181  cnextucn  24188  ucnextcn  24189  cfilresi  25193  cfilres  25194  cmetss  25214  relcmpcmet  25216  cfilucfil3  25218  minveclem4a  25328  filnetlem4  36355