Metamath Proof Explorer

Theorem 2basgen

Description: Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007) (Revised by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	2basgen	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to topGen (B) = topGen (C)$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ topGen (B) \in V$
2	1	ssex	$⊢ C \subseteq topGen (B) \to C \in V$
3		simpl	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to B \subseteq C$
4		tgss	$⊢ (C \in V \land B \subseteq C) \to topGen (B) \subseteq topGen (C)$
5	2 3 4	syl2an2	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to topGen (B) \subseteq topGen (C)$
6		simpr	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to C \subseteq topGen (B)$
7		ssexg	$⊢ (B \subseteq C \land C \in V) \to B \in V$
8	2 7	sylan2	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to B \in V$
9		tgss3	$⊢ (C \in V \land B \in V) \to (topGen (C) \subseteq topGen (B) \leftrightarrow C \subseteq topGen (B))$
10	2 8 9	syl2an2	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to (topGen (C) \subseteq topGen (B) \leftrightarrow C \subseteq topGen (B))$
11	6 10	mpbird	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to topGen (C) \subseteq topGen (B)$
12	5 11	eqssd	$⊢ (B \subseteq C \land C \subseteq topGen (B)) \to topGen (B) = topGen (C)$