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 e. ( Fil ` X ) -> ( fi ` F ) = F )

Proof

Step	Hyp	Ref	Expression
1		filin	|- ( ( F e. ( Fil ` X ) /\ x e. F /\ y e. F ) -> ( x i^i y ) e. F )
2	1	3expib	|- ( F e. ( Fil ` X ) -> ( ( x e. F /\ y e. F ) -> ( x i^i y ) e. F ) )
3	2	ralrimivv	|- ( F e. ( Fil ` X ) -> A. x e. F A. y e. F ( x i^i y ) e. F )
4		inficl	|- ( F e. ( Fil ` X ) -> ( A. x e. F A. y e. F ( x i^i y ) e. F <-> ( fi ` F ) = F ) )
5	3 4	mpbid	|- ( F e. ( Fil ` X ) -> ( fi ` F ) = F )