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 ‘ 𝐵 ) )