Metamath Proof Explorer

Theorem topbas

Description: A topology is its own basis. (Contributed by NM, 17-Jul-2006)

		Ref	Expression
	Assertion	topbas	$⊢ J \in Top \to J \in TopBases$

Proof

Step	Hyp	Ref	Expression
1		inopn	$⊢ (J \in Top \land x \in J \land y \in J) \to x \cap y \in J$
2	1	3expb	$⊢ (J \in Top \land (x \in J \land y \in J)) \to x \cap y \in J$
3		simpr	$⊢ ((J \in Top \land (x \in J \land y \in J)) \land z \in (x \cap y)) \to z \in (x \cap y)$
4		ssid	$⊢ x \cap y \subseteq x \cap y$
5	3 4	jctir	$⊢ ((J \in Top \land (x \in J \land y \in J)) \land z \in (x \cap y)) \to (z \in (x \cap y) \land x \cap y \subseteq x \cap y)$
6		eleq2	$⊢ w = x \cap y \to (z \in w \leftrightarrow z \in (x \cap y))$
7		sseq1	$⊢ w = x \cap y \to (w \subseteq x \cap y \leftrightarrow x \cap y \subseteq x \cap y)$
8	6 7	anbi12d	$⊢ w = x \cap y \to ((z \in w \land w \subseteq x \cap y) \leftrightarrow (z \in (x \cap y) \land x \cap y \subseteq x \cap y))$
9	8	rspcev	$⊢ (x \cap y \in J \land (z \in (x \cap y) \land x \cap y \subseteq x \cap y)) \to \exists w \in J (z \in w \land w \subseteq x \cap y)$
10	2 5 9	syl2an2r	$⊢ ((J \in Top \land (x \in J \land y \in J)) \land z \in (x \cap y)) \to \exists w \in J (z \in w \land w \subseteq x \cap y)$
11	10	exp31	$⊢ J \in Top \to ((x \in J \land y \in J) \to (z \in (x \cap y) \to \exists w \in J (z \in w \land w \subseteq x \cap y)))$
12	11	ralrimdv	$⊢ J \in Top \to ((x \in J \land y \in J) \to \forall z \in (x \cap y) \exists w \in J (z \in w \land w \subseteq x \cap y))$
13	12	ralrimivv	$⊢ J \in Top \to \forall x \in J \forall y \in J \forall z \in (x \cap y) \exists w \in J (z \in w \land w \subseteq x \cap y)$
14		isbasis2g	$⊢ J \in Top \to (J \in TopBases \leftrightarrow \forall x \in J \forall y \in J \forall z \in (x \cap y) \exists w \in J (z \in w \land w \subseteq x \cap y))$
15	13 14	mpbird	$⊢ J \in Top \to J \in TopBases$