This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )