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 ∩ ◡ 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 ) → ( [ 𝐽 ] ∼ = [ 𝐾 ] ∼ ↔ 𝐽 = 𝐾 ) )