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 -1
Assertion topfneec2 ⊢ J ∈ Top ∧ K ∈ Top → J ∼ ˙ = K ∼ ˙ ↔ J = K

Proof

Step Hyp Ref Expression
1 topfneec2.1 ⊢ ∼ ˙ = Fne ∩ Fne -1
2 1 fneval ⊢ J ∈ Top ∧ K ∈ Top → J ∼ ˙ K ↔ topGen ⁡ J = topGen ⁡ K
3 1 fneer ⊢ ∼ ˙ Er V
4 3 a1i ⊢ J ∈ Top ∧ K ∈ Top → ∼ ˙ Er V
5 elex ⊢ J ∈ Top → J ∈ V
6 5 adantr ⊢ J ∈ Top ∧ K ∈ Top → J ∈ V
7 4 6 erth ⊢ J ∈ Top ∧ K ∈ Top → J ∼ ˙ K ↔ J ∼ ˙ = K ∼ ˙
8 tgtop ⊢ J ∈ Top → topGen ⁡ J = J
9 tgtop ⊢ K ∈ Top → topGen ⁡ K = K
10 8 9 eqeqan12d ⊢ J ∈ Top ∧ K ∈ Top → topGen ⁡ J = topGen ⁡ K ↔ J = K
11 2 7 10 3bitr3d ⊢ J ∈ Top ∧ K ∈ Top → J ∼ ˙ = K ∼ ˙ ↔ J = K