![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > filfbas | Structured version Visualization version GIF version |
Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
Ref | Expression |
---|---|
filfbas | ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfil 22452 | . 2 ⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) | |
2 | 1 | simplbi 501 | 1 ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∩ cin 3880 ∅c0 4243 𝒫 cpw 4497 ‘cfv 6324 fBascfbas 20079 Filcfil 22450 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fv 6332 df-fil 22451 |
This theorem is referenced by: 0nelfil 22454 filsspw 22456 filelss 22457 filin 22459 filtop 22460 snfbas 22471 fgfil 22480 elfilss 22481 filfinnfr 22482 fgabs 22484 filconn 22488 fgtr 22495 trfg 22496 ufilb 22511 ufilmax 22512 isufil2 22513 ssufl 22523 ufileu 22524 filufint 22525 ufilen 22535 fmfg 22554 fmufil 22564 fmid 22565 fmco 22566 ufldom 22567 hausflim 22586 flimrest 22588 flimclslem 22589 flfnei 22596 isflf 22598 flfcnp 22609 fclsrest 22629 fclsfnflim 22632 flimfnfcls 22633 isfcf 22639 cnpfcfi 22645 cnpfcf 22646 cnextcn 22672 cfilufg 22899 neipcfilu 22902 cnextucn 22909 ucnextcn 22910 cfilresi 23899 cfilres 23900 cmetss 23920 relcmpcmet 23922 cfilucfil3 23924 minveclem4a 24034 filnetlem4 33842 |
Copyright terms: Public domain | W3C validator |