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 ) )