Theorem filfbas

Description: A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Assertion	filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		isfil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) )
2	1	simplbi	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )