Metamath Proof Explorer

Theorem t0kq

Description: A topological space is T_0 iff the quotient map is a homeomorphism onto the space's Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	t0kq.1	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	t0kq	$⊢ J \in TopOn (X) \to (J \in Kol2 \leftrightarrow F \in (J Homeo KQ (J)))$

Proof

Step	Hyp	Ref	Expression
1		t0kq.1	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		simpl	$⊢ (J \in TopOn (X) \land J \in Kol2) \to J \in TopOn (X)$
3	1	ist0-4	$⊢ J \in TopOn (X) \to (J \in Kol2 \leftrightarrow F : X \underset{1-1}{⟶} V)$
4	3	biimpa	$⊢ (J \in TopOn (X) \land J \in Kol2) \to F : X \underset{1-1}{⟶} V$
5	2 4	qtopf1	$⊢ (J \in TopOn (X) \land J \in Kol2) \to F \in (J Homeo (J qTop F))$
6	1	kqval	$⊢ J \in TopOn (X) \to KQ (J) = J qTop F$
7	6	adantr	$⊢ (J \in TopOn (X) \land J \in Kol2) \to KQ (J) = J qTop F$
8	7	oveq2d	$⊢ (J \in TopOn (X) \land J \in Kol2) \to J Homeo KQ (J) = J Homeo (J qTop F)$
9	5 8	eleqtrrd	$⊢ (J \in TopOn (X) \land J \in Kol2) \to F \in (J Homeo KQ (J))$
10		hmphi	$⊢ F \in (J Homeo KQ (J)) \to J ≃ KQ (J)$
11		hmphsym	$⊢ J ≃ KQ (J) \to KQ (J) ≃ J$
12	10 11	syl	$⊢ F \in (J Homeo KQ (J)) \to KQ (J) ≃ J$
13	1	kqt0lem	$⊢ J \in TopOn (X) \to KQ (J) \in Kol2$
14		t0hmph	$⊢ KQ (J) ≃ J \to (KQ (J) \in Kol2 \to J \in Kol2)$
15	12 13 14	syl2im	$⊢ F \in (J Homeo KQ (J)) \to (J \in TopOn (X) \to J \in Kol2)$
16	15	impcom	$⊢ (J \in TopOn (X) \land F \in (J Homeo KQ (J))) \to J \in Kol2$
17	9 16	impbida	$⊢ J \in TopOn (X) \to (J \in Kol2 \leftrightarrow F \in (J Homeo KQ (J)))$