This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
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 ) )