Theorem filfbas 23905

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

Syntax hints:   → wi 4   ∈ wcel 2142   ≠ wne 2957  ∀wral 3076   ∩ cin 3903  ∅c0 4285  𝒫 cpw 4555  ‘cfv 6521  fBascfbas 21409  Filcfil 23902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fv 6529  df-fil 23903

This theorem is referenced by:  0nelfil  23906  filsspw  23908  filelss  23909  filin  23911  filtop  23912  snfbas  23923  fgfil  23932  elfilss  23933  filfinnfr  23934  fgabs  23936  filconn  23940  fgtr  23947  trfg  23948  ufilb  23963  ufilmax  23964  isufil2  23965  ssufl  23975  ufileu  23976  filufint  23977  ufilen  23987  fmfg  24006  fmufil  24016  fmid  24017  fmco  24018  ufldom  24019  hausflim  24038  flimrest  24040  flimclslem  24041  flfnei  24048  isflf  24050  flfcnp  24061  fclsrest  24081  fclsfnflim  24084  flimfnfcls  24085  isfcf  24091  cnpfcfi  24097  cnpfcf  24098  cnextcn  24124  cfilufg  24349  neipcfilu  24352  cnextucn  24359  ucnextcn  24360  cfilresi  25354  cfilres  25355  cmetss  25375  relcmpcmet  25377  cfilucfil3  25379  minveclem4a  25489  filnetlem4  36738