Theorem tgtopon

Description: A basis generates a topology on U. B . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	tgtopon	⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ ( TopOn ‘ ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		tgcl	⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ Top )
2		unitg	⊢ ( 𝐵 ∈ TopBases → ∪ ( topGen ‘ 𝐵 ) = ∪ 𝐵 )
3	2	eqcomd	⊢ ( 𝐵 ∈ TopBases → ∪ 𝐵 = ∪ ( topGen ‘ 𝐵 ) )
4		istopon	⊢ ( ( topGen ‘ 𝐵 ) ∈ ( TopOn ‘ ∪ 𝐵 ) ↔ ( ( topGen ‘ 𝐵 ) ∈ Top ∧ ∪ 𝐵 = ∪ ( topGen ‘ 𝐵 ) ) )
5	1 3 4	sylanbrc	⊢ ( 𝐵 ∈ TopBases → ( topGen ‘ 𝐵 ) ∈ ( TopOn ‘ ∪ 𝐵 ) )