This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem filfi

Description: A filter is closed under taking intersections. (Contributed by Mario Carneiro, 27-Nov-2013) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filfi	$⊢ F \in Fil (X) \to fi (F) = F$

Step	Hyp	Ref	Expression
1		filin	$⊢ (F \in Fil (X) \land x \in F \land y \in F) \to x \cap y \in F$
2	1	3expib	$⊢ F \in Fil (X) \to ((x \in F \land y \in F) \to x \cap y \in F)$
3	2	ralrimivv	$⊢ F \in Fil (X) \to \forall x \in F \forall y \in F x \cap y \in F$
4		inficl	$⊢ F \in Fil (X) \to (\forall x \in F \forall y \in F x \cap y \in F \leftrightarrow fi (F) = F)$
5	3 4	mpbid	$⊢ F \in Fil (X) \to fi (F) = F$