Theorem filintn0

Description: A filter has the finite intersection property. Remark below Definition 1 of BourbakiTop1 p. I.36. (Contributed by FL, 20-Sep-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filintn0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		elfir	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ∈ ( fi ‘ 𝐹 ) )
2		filfi	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = 𝐹 )
3	2	adantr	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ( fi ‘ 𝐹 ) = 𝐹 )
4	1 3	eleqtrd	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ∈ 𝐹 )
5		fileln0	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∩ 𝐴 ∈ 𝐹 ) → ∩ 𝐴 ≠ ∅ )
6	4 5	syldan	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ≠ ∅ )