eltg3i

Description: The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	eltg3i	$⊢ (B \in V \land A \subseteq B) \to ⋃ A \in topGen (B)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in V \land A \subseteq B) \to A \subseteq B$
2		pwuni	$⊢ A \subseteq 𝒫 ⋃ A$
3		ssin	$⊢ (A \subseteq B \land A \subseteq 𝒫 ⋃ A) \leftrightarrow A \subseteq B \cap 𝒫 ⋃ A$
4	1 2 3	sylanblc	$⊢ (B \in V \land A \subseteq B) \to A \subseteq B \cap 𝒫 ⋃ A$
5	4	unissd	$⊢ (B \in V \land A \subseteq B) \to ⋃ A \subseteq ⋃ (B \cap 𝒫 ⋃ A)$
6		eltg	$⊢ B \in V \to (⋃ A \in topGen (B) \leftrightarrow ⋃ A \subseteq ⋃ (B \cap 𝒫 ⋃ A))$
7	6	adantr	$⊢ (B \in V \land A \subseteq B) \to (⋃ A \in topGen (B) \leftrightarrow ⋃ A \subseteq ⋃ (B \cap 𝒫 ⋃ A))$
8	5 7	mpbird	$⊢ (B \in V \land A \subseteq B) \to ⋃ A \in topGen (B)$

Metamath Proof Explorer