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 ∩ ◡ Fne )
Assertion	topfneec2	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( [ 𝐽 ] ∼ = [ 𝐾 ] ∼ ↔ 𝐽 = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		topfneec2.1	⊢ ∼ = ( Fne ∩ ◡ Fne )
2	1	fneval	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∼ 𝐾 ↔ ( topGen ‘ 𝐽 ) = ( topGen ‘ 𝐾 ) ) )
3	1	fneer	⊢ ∼ Er V
4	3	a1i	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ∼ Er V )
5		elex	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ V )
6	5	adantr	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → 𝐽 ∈ V )
7	4 6	erth	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ∼ 𝐾 ↔ [ 𝐽 ] ∼ = [ 𝐾 ] ∼ ) )
8		tgtop	⊢ ( 𝐽 ∈ Top → ( topGen ‘ 𝐽 ) = 𝐽 )
9		tgtop	⊢ ( 𝐾 ∈ Top → ( topGen ‘ 𝐾 ) = 𝐾 )
10	8 9	eqeqan12d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( ( topGen ‘ 𝐽 ) = ( topGen ‘ 𝐾 ) ↔ 𝐽 = 𝐾 ) )
11	2 7 10	3bitr3d	⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( [ 𝐽 ] ∼ = [ 𝐾 ] ∼ ↔ 𝐽 = 𝐾 ) )