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

Metamath Proof Explorer

Theorem topfneec2

Description: A topology is precisely identified with its equivalence class. (Contributed by Jeff Hankins, 12-Oct-2009)

Ref Expression
Hypothesis topfneec2.1 
|- .~ = ( Fne i^i `' Fne )
Assertion topfneec2 
|- ( ( J e. Top /\ K e. Top ) -> ( [ J ] .~ = [ K ] .~ <-> J = K ) )

Proof

Step Hyp Ref Expression
1 topfneec2.1 
 |-  .~ = ( Fne i^i `' Fne )
2 1 fneval 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J .~ K <-> ( topGen ` J ) = ( topGen ` K ) ) )
3 1 fneer 
 |-  .~ Er _V
4 3 a1i 
 |-  ( ( J e. Top /\ K e. Top ) -> .~ Er _V )
5 elex 
 |-  ( J e. Top -> J e. _V )
6 5 adantr 
 |-  ( ( J e. Top /\ K e. Top ) -> J e. _V )
7 4 6 erth 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J .~ K <-> [ J ] .~ = [ K ] .~ ) )
8 tgtop 
 |-  ( J e. Top -> ( topGen ` J ) = J )
9 tgtop 
 |-  ( K e. Top -> ( topGen ` K ) = K )
10 8 9 eqeqan12d 
 |-  ( ( J e. Top /\ K e. Top ) -> ( ( topGen ` J ) = ( topGen ` K ) <-> J = K ) )
11 2 7 10 3bitr3d 
 |-  ( ( J e. Top /\ K e. Top ) -> ( [ J ] .~ = [ K ] .~ <-> J = K ) )