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	$⊢ (F \in fBas (X) \land A \in F \land B \in F) \to \exists x \in F x \subseteq A \cap B$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
2		isfbas2	$⊢ X \in dom fBas \to (F \in fBas (X) \leftrightarrow (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z)))$
3	1 2	syl	$⊢ F \in fBas (X) \to (F \in fBas (X) \leftrightarrow (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z)))$
4	3	ibi	$⊢ F \in fBas (X) \to (F \subseteq 𝒫 X \land (F \neq \emptyset \land \emptyset \notin F \land \forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z))$
5	4	simprd	$⊢ F \in fBas (X) \to (F \neq \emptyset \land \emptyset \notin F \land \forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z)$
6	5	simp3d	$⊢ F \in fBas (X) \to \forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z$
7		ineq1	$⊢ y = A \to y \cap z = A \cap z$
8	7	sseq2d	$⊢ y = A \to (x \subseteq y \cap z \leftrightarrow x \subseteq A \cap z)$
9	8	rexbidv	$⊢ y = A \to (\exists x \in F x \subseteq y \cap z \leftrightarrow \exists x \in F x \subseteq A \cap z)$
10		ineq2	$⊢ z = B \to A \cap z = A \cap B$
11	10	sseq2d	$⊢ z = B \to (x \subseteq A \cap z \leftrightarrow x \subseteq A \cap B)$
12	11	rexbidv	$⊢ z = B \to (\exists x \in F x \subseteq A \cap z \leftrightarrow \exists x \in F x \subseteq A \cap B)$
13	9 12	rspc2v	$⊢ (A \in F \land B \in F) \to (\forall y \in F \forall z \in F \exists x \in F x \subseteq y \cap z \to \exists x \in F x \subseteq A \cap B)$
14	6 13	syl5com	$⊢ F \in fBas (X) \to ((A \in F \land B \in F) \to \exists x \in F x \subseteq A \cap B)$
15	14	3impib	$⊢ (F \in fBas (X) \land A \in F \land B \in F) \to \exists x \in F x \subseteq A \cap B$