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	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		filin	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
2	1	3expib	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) )
3	2	ralrimivv	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
4		inficl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ↔ ( fi ‘ 𝐹 ) = 𝐹 ) )
5	3 4	mpbid	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( fi ‘ 𝐹 ) = 𝐹 )