filin

Description: A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filin	$⊢ (F \in Fil (X) \land A \in F \land B \in F) \to A \cap B \in F$

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		fbasssin	$⊢ (F \in fBas (X) \land A \in F \land B \in F) \to \exists x \in F x \subseteq A \cap B$
3	1 2	syl3an1	$⊢ (F \in Fil (X) \land A \in F \land B \in F) \to \exists x \in F x \subseteq A \cap B$
4		inss1	$⊢ A \cap B \subseteq A$
5		filelss	$⊢ (F \in Fil (X) \land A \in F) \to A \subseteq X$
6	4 5	sstrid	$⊢ (F \in Fil (X) \land A \in F) \to A \cap B \subseteq X$
7		filss	$⊢ (F \in Fil (X) \land (x \in F \land A \cap B \subseteq X \land x \subseteq A \cap B)) \to A \cap B \in F$
8	7	3exp2	$⊢ F \in Fil (X) \to (x \in F \to (A \cap B \subseteq X \to (x \subseteq A \cap B \to A \cap B \in F)))$
9	8	com23	$⊢ F \in Fil (X) \to (A \cap B \subseteq X \to (x \in F \to (x \subseteq A \cap B \to A \cap B \in F)))$
10	9	imp	$⊢ (F \in Fil (X) \land A \cap B \subseteq X) \to (x \in F \to (x \subseteq A \cap B \to A \cap B \in F))$
11	10	rexlimdv	$⊢ (F \in Fil (X) \land A \cap B \subseteq X) \to (\exists x \in F x \subseteq A \cap B \to A \cap B \in F)$
12	6 11	syldan	$⊢ (F \in Fil (X) \land A \in F) \to (\exists x \in F x \subseteq A \cap B \to A \cap B \in F)$
13	12	3adant3	$⊢ (F \in Fil (X) \land A \in F \land B \in F) \to (\exists x \in F x \subseteq A \cap B \to A \cap B \in F)$
14	3 13	mpd	$⊢ (F \in Fil (X) \land A \in F \land B \in F) \to A \cap B \in F$

Metamath Proof Explorer