Metamath Proof Explorer

Theorem basgen2

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. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	basgen2	$⊢ (J \in Top \land B \subseteq J \land \forall x \in J \forall y \in x \exists z \in B (y \in z \land z \subseteq x)) \to topGen (B) = J$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$⊢ J \subseteq topGen (B) \leftrightarrow \forall x \in J x \in topGen (B)$
2		ssexg	$⊢ (B \subseteq J \land J \in Top) \to B \in V$
3	2	ancoms	$⊢ (J \in Top \land B \subseteq J) \to B \in V$
4		eltg2b	$⊢ B \in V \to (x \in topGen (B) \leftrightarrow \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
5	3 4	syl	$⊢ (J \in Top \land B \subseteq J) \to (x \in topGen (B) \leftrightarrow \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
6	5	ralbidv	$⊢ (J \in Top \land B \subseteq J) \to (\forall x \in J x \in topGen (B) \leftrightarrow \forall x \in J \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
7	1 6	bitrid	$⊢ (J \in Top \land B \subseteq J) \to (J \subseteq topGen (B) \leftrightarrow \forall x \in J \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
8	7	biimp3ar	$⊢ (J \in Top \land B \subseteq J \land \forall x \in J \forall y \in x \exists z \in B (y \in z \land z \subseteq x)) \to J \subseteq topGen (B)$
9		basgen	$⊢ (J \in Top \land B \subseteq J \land J \subseteq topGen (B)) \to topGen (B) = J$
10	8 9	syld3an3	$⊢ (J \in Top \land B \subseteq J \land \forall x \in J \forall y \in x \exists z \in B (y \in z \land z \subseteq x)) \to topGen (B) = J$