tgtop

		Ref	Expression
	Assertion	tgtop	$⊢ J \in Top \to topGen (J) = J$

Step	Hyp	Ref	Expression
1		eltg3	$⊢ J \in Top \to (x \in topGen (J) \leftrightarrow \exists y (y \subseteq J \land x = ⋃ y))$
2		simpr	$⊢ ((J \in Top \land y \subseteq J) \land x = ⋃ y) \to x = ⋃ y$
3		uniopn	$⊢ (J \in Top \land y \subseteq J) \to ⋃ y \in J$
4	3	adantr	$⊢ ((J \in Top \land y \subseteq J) \land x = ⋃ y) \to ⋃ y \in J$
5	2 4	eqeltrd	$⊢ ((J \in Top \land y \subseteq J) \land x = ⋃ y) \to x \in J$
6	5	expl	$⊢ J \in Top \to ((y \subseteq J \land x = ⋃ y) \to x \in J)$
7	6	exlimdv	$⊢ J \in Top \to (\exists y (y \subseteq J \land x = ⋃ y) \to x \in J)$
8	1 7	sylbid	$⊢ J \in Top \to (x \in topGen (J) \to x \in J)$
9	8	ssrdv	$⊢ J \in Top \to topGen (J) \subseteq J$
10		bastg	$⊢ J \in Top \to J \subseteq topGen (J)$
11	9 10	eqssd	$⊢ J \in Top \to topGen (J) = J$

Metamath Proof Explorer