tgss

Description: Subset relation for generated topologies. (Contributed by NM, 7-May-2007)

		Ref	Expression
	Assertion	tgss	$⊢ (C \in V \land B \subseteq C) \to topGen (B) \subseteq topGen (C)$

Step	Hyp	Ref	Expression
1		ssrin	$⊢ B \subseteq C \to B \cap 𝒫 x \subseteq C \cap 𝒫 x$
2	1	unissd	$⊢ B \subseteq C \to ⋃ (B \cap 𝒫 x) \subseteq ⋃ (C \cap 𝒫 x)$
3		sstr2	$⊢ x \subseteq ⋃ (B \cap 𝒫 x) \to (⋃ (B \cap 𝒫 x) \subseteq ⋃ (C \cap 𝒫 x) \to x \subseteq ⋃ (C \cap 𝒫 x))$
4	2 3	syl5com	$⊢ B \subseteq C \to (x \subseteq ⋃ (B \cap 𝒫 x) \to x \subseteq ⋃ (C \cap 𝒫 x))$
5	4	adantl	$⊢ (C \in V \land B \subseteq C) \to (x \subseteq ⋃ (B \cap 𝒫 x) \to x \subseteq ⋃ (C \cap 𝒫 x))$
6		ssexg	$⊢ (B \subseteq C \land C \in V) \to B \in V$
7	6	ancoms	$⊢ (C \in V \land B \subseteq C) \to B \in V$
8		eltg	$⊢ B \in V \to (x \in topGen (B) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x))$
9	7 8	syl	$⊢ (C \in V \land B \subseteq C) \to (x \in topGen (B) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x))$
10		eltg	$⊢ C \in V \to (x \in topGen (C) \leftrightarrow x \subseteq ⋃ (C \cap 𝒫 x))$
11	10	adantr	$⊢ (C \in V \land B \subseteq C) \to (x \in topGen (C) \leftrightarrow x \subseteq ⋃ (C \cap 𝒫 x))$
12	5 9 11	3imtr4d	$⊢ (C \in V \land B \subseteq C) \to (x \in topGen (B) \to x \in topGen (C))$
13	12	ssrdv	$⊢ (C \in V \land B \subseteq C) \to topGen (B) \subseteq topGen (C)$

Metamath Proof Explorer