Theorem filinn0

Description: The intersection of two elements of a filter can't be empty. (Contributed by FL, 16-Sep-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filinn0	|- ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( A i^i B ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> F e. ( Fil ` X ) )
2		filin	|- ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( A i^i B ) e. F )
3		fileln0	|- ( ( F e. ( Fil ` X ) /\ ( A i^i B ) e. F ) -> ( A i^i B ) =/= (/) )
4	1 2 3	syl2anc	|- ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( A i^i B ) =/= (/) )