tg1

Description: Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006)

		Ref	Expression
	Assertion	tg1	$⊢ A \in topGen (B) \to A \subseteq ⋃ B$

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ A \in topGen (B) \to B \in dom topGen$
2		eltg2	$⊢ B \in dom topGen \to (A \in topGen (B) \leftrightarrow (A \subseteq ⋃ B \land \forall x \in A \exists y \in B (x \in y \land y \subseteq A)))$
3	2	simprbda	$⊢ (B \in dom topGen \land A \in topGen (B)) \to A \subseteq ⋃ B$
4	1 3	mpancom	$⊢ A \in topGen (B) \to A \subseteq ⋃ B$

Metamath Proof Explorer