# Metamath Proof Explorer

## Theorem fbasssin

Description: A filter base contains subsets of its pairwise intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Jeff Hankins, 1-Dec-2010)

Ref Expression
Assertion fbasssin ${⊢}\left({F}\in \mathrm{fBas}\left({X}\right)\wedge {A}\in {F}\wedge {B}\in {F}\right)\to \exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {B}$

### Proof

Step Hyp Ref Expression
1 elfvdm ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to {X}\in \mathrm{dom}\mathrm{fBas}$
2 isfbas2 ${⊢}{X}\in \mathrm{dom}\mathrm{fBas}\to \left({F}\in \mathrm{fBas}\left({X}\right)↔\left({F}\subseteq 𝒫{X}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}\right)\right)\right)$
3 1 2 syl ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to \left({F}\in \mathrm{fBas}\left({X}\right)↔\left({F}\subseteq 𝒫{X}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}\right)\right)\right)$
4 3 ibi ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to \left({F}\subseteq 𝒫{X}\wedge \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}\right)\right)$
5 4 simprd ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to \left({F}\ne \varnothing \wedge \varnothing \notin {F}\wedge \forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}\right)$
6 5 simp3d ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to \forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}$
7 ineq1 ${⊢}{y}={A}\to {y}\cap {z}={A}\cap {z}$
8 7 sseq2d ${⊢}{y}={A}\to \left({x}\subseteq {y}\cap {z}↔{x}\subseteq {A}\cap {z}\right)$
9 8 rexbidv ${⊢}{y}={A}\to \left(\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}↔\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {z}\right)$
10 ineq2 ${⊢}{z}={B}\to {A}\cap {z}={A}\cap {B}$
11 10 sseq2d ${⊢}{z}={B}\to \left({x}\subseteq {A}\cap {z}↔{x}\subseteq {A}\cap {B}\right)$
12 11 rexbidv ${⊢}{z}={B}\to \left(\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {z}↔\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {B}\right)$
13 9 12 rspc2v ${⊢}\left({A}\in {F}\wedge {B}\in {F}\right)\to \left(\forall {y}\in {F}\phantom{\rule{.4em}{0ex}}\forall {z}\in {F}\phantom{\rule{.4em}{0ex}}\exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\cap {z}\to \exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {B}\right)$
14 6 13 syl5com ${⊢}{F}\in \mathrm{fBas}\left({X}\right)\to \left(\left({A}\in {F}\wedge {B}\in {F}\right)\to \exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {B}\right)$
15 14 3impib ${⊢}\left({F}\in \mathrm{fBas}\left({X}\right)\wedge {A}\in {F}\wedge {B}\in {F}\right)\to \exists {x}\in {F}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\cap {B}$