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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion	ist0-4	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ 𝐹 : 𝑋 –1-1→ V ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2	1	kqfeq	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ) )
3	2	3expb	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) ) )
4	3	imbi1d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) → 𝑧 = 𝑤 ) ) )
5	4	2ralbidva	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) → 𝑧 = 𝑤 ) ) )
6	1	kqffn	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
7		dffn2	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 ⟶ V )
8	6 7	sylib	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 : 𝑋 ⟶ V )
9		dff13	⊢ ( 𝐹 : 𝑋 –1-1→ V ↔ ( 𝐹 : 𝑋 ⟶ V ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
10	9	baib	⊢ ( 𝐹 : 𝑋 ⟶ V → ( 𝐹 : 𝑋 –1-1→ V ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
11	8 10	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐹 : 𝑋 –1-1→ V ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
12		ist0-2	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ ∀ 𝑧 ∈ 𝑋 ∀ 𝑤 ∈ 𝑋 ( ∀ 𝑦 ∈ 𝐽 ( 𝑧 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) → 𝑧 = 𝑤 ) ) )
13	5 11 12	3bitr4rd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Kol2 ↔ 𝐹 : 𝑋 –1-1→ V ) )