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-1V

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∈Jz∈y↔w∈y
3 2 3expb ⊢J∈TopOn⁡X∧z∈X∧w∈X→F⁡z=F⁡w↔∀y∈Jz∈y↔w∈y
4 3 imbi1d ⊢J∈TopOn⁡X∧z∈X∧w∈X→F⁡z=F⁡w→z=w↔∀y∈Jz∈y↔w∈y→z=w
5 4 2ralbidva ⊢J∈TopOn⁡X→∀z∈X∀w∈XF⁡z=F⁡w→z=w↔∀z∈X∀w∈X∀y∈Jz∈y↔w∈y→z=w
6 1 kqffn ⊢J∈TopOn⁡X→FFnX
7 dffn2 ⊢FFnX↔F:X⟶V
8 6 7 sylib ⊢J∈TopOn⁡X→F:X⟶V
9 dff13 ⊢F:X⟶1-1V↔F:X⟶V∧∀z∈X∀w∈XF⁡z=F⁡w→z=w
10 9 baib ⊢F:X⟶V→F:X⟶1-1V↔∀z∈X∀w∈XF⁡z=F⁡w→z=w
11 8 10 syl ⊢J∈TopOn⁡X→F:X⟶1-1V↔∀z∈X∀w∈XF⁡z=F⁡w→z=w
12 ist0-2 ⊢J∈TopOn⁡X→J∈Kol2↔∀z∈X∀w∈X∀y∈Jz∈y↔w∈y→z=w
13 5 11 12 3bitr4rd ⊢J∈TopOn⁡X→J∈Kol2↔F:X⟶1-1V