Theorem tgtop

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

	Ref	Expression
Assertion	tgtop	|- ( J e. Top -> ( topGen ` J ) = J )

Proof

Step	Hyp	Ref	Expression
1		eltg3	|- ( J e. Top -> ( x e. ( topGen ` J ) <-> E. y ( y C_ J /\ x = U. y ) ) )
2		simpr	|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> x = U. y )
3		uniopn	|- ( ( J e. Top /\ y C_ J ) -> U. y e. J )
4	3	adantr	|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> U. y e. J )
5	2 4	eqeltrd	|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> x e. J )
6	5	expl	|- ( J e. Top -> ( ( y C_ J /\ x = U. y ) -> x e. J ) )
7	6	exlimdv	|- ( J e. Top -> ( E. y ( y C_ J /\ x = U. y ) -> x e. J ) )
8	1 7	sylbid	|- ( J e. Top -> ( x e. ( topGen ` J ) -> x e. J ) )
9	8	ssrdv	|- ( J e. Top -> ( topGen ` J ) C_ J )
10		bastg	|- ( J e. Top -> J C_ ( topGen ` J ) )
11	9 10	eqssd	|- ( J e. Top -> ( topGen ` J ) = J )