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	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2		filin	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 )
3		fileln0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
4	1 2 3	syl2anc	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )