This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bastg

Description: A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion bastg ( 𝐵 ∈ 𝑉 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
2 vex ⊢ 𝑥 ∈ V
3 2 pwid ⊢ 𝑥 ∈ 𝒫 𝑥
4 3 a1i ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝒫 𝑥 )
5 1 4 elind ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) )
6 elssuni ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
7 5 6 syl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
8 7 ex ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
9 eltg ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
10 8 9 sylibrd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
11 10 ssrdv ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )