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	$⊢ B \in V \to B \subseteq topGen (B)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in V \land x \in B) \to x \in B$
2		vex	$⊢ x \in V$
3	2	pwid	$⊢ x \in 𝒫 x$
4	3	a1i	$⊢ (B \in V \land x \in B) \to x \in 𝒫 x$
5	1 4	elind	$⊢ (B \in V \land x \in B) \to x \in (B \cap 𝒫 x)$
6		elssuni	$⊢ x \in (B \cap 𝒫 x) \to x \subseteq ⋃ (B \cap 𝒫 x)$
7	5 6	syl	$⊢ (B \in V \land x \in B) \to x \subseteq ⋃ (B \cap 𝒫 x)$
8	7	ex	$⊢ B \in V \to (x \in B \to x \subseteq ⋃ (B \cap 𝒫 x))$
9		eltg	$⊢ B \in V \to (x \in topGen (B) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x))$
10	8 9	sylibrd	$⊢ B \in V \to (x \in B \to x \in topGen (B))$
11	10	ssrdv	$⊢ B \in V \to B \subseteq topGen (B)$