Theorem tgtop

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

	Ref	Expression
Assertion	tgtop	$$⊢J\in \mathrm{Top}\to \mathrm{topGen}\left(J\right)=J$$

Proof

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