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 \mathrm{Fil}\left(X\right)\to \mathrm{fi}\left(F\right)=F$$

Proof

Step	Hyp	Ref	Expression
1		filin	$$⊢\left(F\in \mathrm{Fil}\left(X\right)\wedge x\in F\wedge y\in F\right)\to x\cap y\in F$$
2	1	3expib	$$⊢F\in \mathrm{Fil}\left(X\right)\to \left(\left(x\in F\wedge y\in F\right)\to x\cap y\in F\right)$$
3	2	ralrimivv	$$⊢F\in \mathrm{Fil}\left(X\right)\to \forall x\in F\forall y\in Fx\cap y\in F$$
4		inficl	$$⊢F\in \mathrm{Fil}\left(X\right)\to \left(\forall x\in F\forall y\in Fx\cap y\in F\leftrightarrow \mathrm{fi}\left(F\right)=F\right)$$
5	3 4	mpbid	$$⊢F\in \mathrm{Fil}\left(X\right)\to \mathrm{fi}\left(F\right)=F$$