Theorem fibas

Description: A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009) (Revised by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Assertion	fibas	⊢ ( fi ‘ 𝐴 ) ∈ TopBases

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( fi ‘ 𝐴 ) ∈ V
2		fiin	⊢ ( ( 𝑥 ∈ ( fi ‘ 𝐴 ) ∧ 𝑦 ∈ ( fi ‘ 𝐴 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) )
3	2	rgen2	⊢ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 )
4		fiinbas	⊢ ( ( ( fi ‘ 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ ( fi ‘ 𝐴 ) ∀ 𝑦 ∈ ( fi ‘ 𝐴 ) ( 𝑥 ∩ 𝑦 ) ∈ ( fi ‘ 𝐴 ) ) → ( fi ‘ 𝐴 ) ∈ TopBases )
5	1 3 4	mp2an	⊢ ( fi ‘ 𝐴 ) ∈ TopBases