Metamath Proof Explorer

Theorem ist0-4

Description: The topological indistinguishability map is injective iff the space is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion ist0-4 ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ F : X ⟶ 1-1 V

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 1 kqfeq ⊢ J ∈ TopOn ⁡ X ∧ z ∈ X ∧ w ∈ X → F ⁡ z = F ⁡ w ↔ ∀ y ∈ J z ∈ y ↔ w ∈ y
3 2 3expb ⊢ J ∈ TopOn ⁡ X ∧ z ∈ X ∧ w ∈ X → F ⁡ z = F ⁡ w ↔ ∀ y ∈ J z ∈ y ↔ w ∈ y
4 3 imbi1d ⊢ J ∈ TopOn ⁡ X ∧ z ∈ X ∧ w ∈ X → F ⁡ z = F ⁡ w → z = w ↔ ∀ y ∈ J z ∈ y ↔ w ∈ y → z = w
5 4 2ralbidva ⊢ J ∈ TopOn ⁡ X → ∀ z ∈ X ∀ w ∈ X F ⁡ z = F ⁡ w → z = w ↔ ∀ z ∈ X ∀ w ∈ X ∀ y ∈ J z ∈ y ↔ w ∈ y → z = w
6 1 kqffn ⊢ J ∈ TopOn ⁡ X → F Fn X
7 dffn2 ⊢ F Fn X ↔ F : X ⟶ V
8 6 7 sylib ⊢ J ∈ TopOn ⁡ X → F : X ⟶ V
9 dff13 ⊢ F : X ⟶ 1-1 V ↔ F : X ⟶ V ∧ ∀ z ∈ X ∀ w ∈ X F ⁡ z = F ⁡ w → z = w
10 9 baib ⊢ F : X ⟶ V → F : X ⟶ 1-1 V ↔ ∀ z ∈ X ∀ w ∈ X F ⁡ z = F ⁡ w → z = w
11 8 10 syl ⊢ J ∈ TopOn ⁡ X → F : X ⟶ 1-1 V ↔ ∀ z ∈ X ∀ w ∈ X F ⁡ z = F ⁡ w → z = w
12 ist0-2 ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ ∀ z ∈ X ∀ w ∈ X ∀ y ∈ J z ∈ y ↔ w ∈ y → z = w
13 5 11 12 3bitr4rd ⊢ J ∈ TopOn ⁡ X → J ∈ Kol2 ↔ F : X ⟶ 1-1 V