bastop2

Description: A version of bastop1 that doesn't have B C_ J in the antecedent. (Contributed by NM, 3-Feb-2008)

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

Step	Hyp	Ref	Expression
1		eleq1	$⊢ topGen (B) = J \to (topGen (B) \in Top \leftrightarrow J \in Top)$
2	1	biimparc	$⊢ (J \in Top \land topGen (B) = J) \to topGen (B) \in Top$
3		tgclb	$⊢ B \in TopBases \leftrightarrow topGen (B) \in Top$
4	2 3	sylibr	$⊢ (J \in Top \land topGen (B) = J) \to B \in TopBases$
5		bastg	$⊢ B \in TopBases \to B \subseteq topGen (B)$
6	4 5	syl	$⊢ (J \in Top \land topGen (B) = J) \to B \subseteq topGen (B)$
7		simpr	$⊢ (J \in Top \land topGen (B) = J) \to topGen (B) = J$
8	6 7	sseqtrd	$⊢ (J \in Top \land topGen (B) = J) \to B \subseteq J$
9	8	ex	$⊢ J \in Top \to (topGen (B) = J \to B \subseteq J)$
10	9	pm4.71rd	$⊢ J \in Top \to (topGen (B) = J \leftrightarrow (B \subseteq J \land topGen (B) = J))$
11		bastop1	$⊢ (J \in Top \land B \subseteq J) \to (topGen (B) = J \leftrightarrow \forall x \in J \exists y (y \subseteq B \land x = ⋃ y))$
12	11	pm5.32da	$⊢ J \in Top \to ((B \subseteq J \land topGen (B) = J) \leftrightarrow (B \subseteq J \land \forall x \in J \exists y (y \subseteq B \land x = ⋃ y)))$
13	10 12	bitrd	$⊢ J \in Top \to (topGen (B) = J \leftrightarrow (B \subseteq J \land \forall x \in J \exists y (y \subseteq B \land x = ⋃ y)))$

Metamath Proof Explorer