Metamath Proof Explorer

Theorem tgtop11

Description: The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006)

Ref Expression
Assertion tgtop11 
|- ( ( J e. Top /\ K e. Top /\ ( topGen ` J ) = ( topGen ` K ) ) -> J = K )

Proof

Step Hyp Ref Expression
1 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
2 tgtop 
 |-  ( K e. Top -> ( topGen ` K ) = K )
3 1 2 eqeqan12d 
 |-  ( ( J e. Top /\ K e. Top ) -> ( ( topGen ` J ) = ( topGen ` K ) <-> J = K ) )
4 3 biimp3a 
 |-  ( ( J e. Top /\ K e. Top /\ ( topGen ` J ) = ( topGen ` K ) ) -> J = K )