Metamath Proof Explorer

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 ⁡ A ∈ TopBases

Proof

Step Hyp Ref Expression
1 fvex ⊢ fi ⁡ A ∈ V
2 fiin ⊢ x ∈ fi ⁡ A ∧ y ∈ fi ⁡ A → x ∩ y ∈ fi ⁡ A
3 2 rgen2 ⊢ ∀ x ∈ fi ⁡ A ∀ y ∈ fi ⁡ A x ∩ y ∈ fi ⁡ A
4 fiinbas ⊢ fi ⁡ A ∈ V ∧ ∀ x ∈ fi ⁡ A ∀ y ∈ fi ⁡ A x ∩ y ∈ fi ⁡ A → fi ⁡ A ∈ TopBases
5 1 3 4 mp2an ⊢ fi ⁡ A ∈ TopBases