Metamath Proof Explorer

Theorem tgss3

Description: A criterion for determining whether one topology is finer than another. Lemma 2.2 of Munkres p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		bastg	$⊢ B \in V \to B \subseteq topGen (B)$
2	1	adantr	$⊢ (B \in V \land C \in W) \to B \subseteq topGen (B)$
3		sstr2	$⊢ B \subseteq topGen (B) \to (topGen (B) \subseteq topGen (C) \to B \subseteq topGen (C))$
4	2 3	syl	$⊢ (B \in V \land C \in W) \to (topGen (B) \subseteq topGen (C) \to B \subseteq topGen (C))$
5		fvex	$⊢ topGen (C) \in V$
6		tgss	$⊢ (topGen (C) \in V \land B \subseteq topGen (C)) \to topGen (B) \subseteq topGen (topGen (C))$
7	5 6	mpan	$⊢ B \subseteq topGen (C) \to topGen (B) \subseteq topGen (topGen (C))$
8		tgidm	$⊢ C \in W \to topGen (topGen (C)) = topGen (C)$
9	8	adantl	$⊢ (B \in V \land C \in W) \to topGen (topGen (C)) = topGen (C)$
10	9	sseq2d	$⊢ (B \in V \land C \in W) \to (topGen (B) \subseteq topGen (topGen (C)) \leftrightarrow topGen (B) \subseteq topGen (C))$
11	7 10	imbitrid	$⊢ (B \in V \land C \in W) \to (B \subseteq topGen (C) \to topGen (B) \subseteq topGen (C))$
12	4 11	impbid	$⊢ (B \in V \land C \in W) \to (topGen (B) \subseteq topGen (C) \leftrightarrow B \subseteq topGen (C))$