This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Topology Topological bases 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