Metamath Proof Explorer

Theorem basgen

Description: Given a topology J , show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of Munkres p. 81 using abbreviations. (Contributed by NM, 22-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	basgen	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (B) = J$

Proof

Step	Hyp	Ref	Expression
1		tgss	$⊢ (J \in Top \land B \subseteq J) \to topGen (B) \subseteq topGen (J)$
2	1	3adant3	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (B) \subseteq topGen (J)$
3		tgtop	$⊢ J \in Top \to topGen (J) = J$
4	3	3ad2ant1	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (J) = J$
5	2 4	sseqtrd	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (B) \subseteq J$
6		simp3	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to J \subseteq topGen (B)$
7	5 6	eqssd	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (B) = J$