# Metamath Proof Explorer

## Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion isfbas2 ${⊢}{B}\in {A}\to \left({F}\in \mathrm{fBas}\left({B}\right)↔\left({F}\subseteq 𝒫{B}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 isfbas ${⊢}{B}\in {A}\to \left({F}\in \mathrm{fBas}\left({B}\right)↔\left({F}\subseteq 𝒫{B}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing \right)\right)\right)$
2 elin ${⊢}{z}\in \left({F}\cap 𝒫\left({x}\cap {y}\right)\right)↔\left({z}\in {F}\wedge {z}\in 𝒫\left({x}\cap {y}\right)\right)$
3 velpw ${⊢}{z}\in 𝒫\left({x}\cap {y}\right)↔{z}\subseteq {x}\cap {y}$
4 3 anbi2i ${⊢}\left({z}\in {F}\wedge {z}\in 𝒫\left({x}\cap {y}\right)\right)↔\left({z}\in {F}\wedge {z}\subseteq {x}\cap {y}\right)$
5 2 4 bitri ${⊢}{z}\in \left({F}\cap 𝒫\left({x}\cap {y}\right)\right)↔\left({z}\in {F}\wedge {z}\subseteq {x}\cap {y}\right)$
6 5 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({F}\cap 𝒫\left({x}\cap {y}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {F}\wedge {z}\subseteq {x}\cap {y}\right)$
7 n0 ${⊢}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing ↔\exists {z}\phantom{\rule{.4em}{0ex}}{z}\in \left({F}\cap 𝒫\left({x}\cap {y}\right)\right)$
8 df-rex ${⊢}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {F}\wedge {z}\subseteq {x}\cap {y}\right)$
9 6 7 8 3bitr4i ${⊢}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing ↔\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}$
10 9 2ralbii ${⊢}\forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing ↔\forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}$
11 10 3anbi3i ${⊢}\left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing \right)↔\left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}\right)$
12 11 anbi2i ${⊢}\left({F}\subseteq 𝒫{B}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}{F}\cap 𝒫\left({x}\cap {y}\right)\ne \varnothing \right)\right)↔\left({F}\subseteq 𝒫{B}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}\right)\right)$
13 1 12 syl6bb ${⊢}{B}\in {A}\to \left({F}\in \mathrm{fBas}\left({B}\right)↔\left({F}\subseteq 𝒫{B}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\exists {z}\in {F}\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}\right)\right)\right)$