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

Metamath Proof Explorer

Theorem t1t0

Description: A T_1 space is a T_0 space. (Contributed by Jeff Hankins, 1-Feb-2010)

		Ref	Expression
	Assertion	t1t0	$⊢ J \in Fre \to J \in Kol2$

Proof

Step	Hyp	Ref	Expression
1		t1top	$⊢ J \in Fre \to J \in Top$
2		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
3	1 2	sylib	$⊢ J \in Fre \to J \in TopOn (⋃ J)$
4		biimp	$⊢ (x \in o \leftrightarrow y \in o) \to (x \in o \to y \in o)$
5	4	ralimi	$⊢ \forall o \in J (x \in o \leftrightarrow y \in o) \to \forall o \in J (x \in o \to y \in o)$
6	5	imim1i	$⊢ (\forall o \in J (x \in o \to y \in o) \to x = y) \to (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y)$
7	6	ralimi	$⊢ \forall y \in ⋃ J (\forall o \in J (x \in o \to y \in o) \to x = y) \to \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y)$
8	7	ralimi	$⊢ \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \to y \in o) \to x = y) \to \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y)$
9	8	a1i	$⊢ J \in TopOn (⋃ J) \to (\forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \to y \in o) \to x = y) \to \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y))$
10		ist1-2	$⊢ J \in TopOn (⋃ J) \to (J \in Fre \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \to y \in o) \to x = y))$
11		ist0-2	$⊢ J \in TopOn (⋃ J) \to (J \in Kol2 \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y))$
12	9 10 11	3imtr4d	$⊢ J \in TopOn (⋃ J) \to (J \in Fre \to J \in Kol2)$
13	3 12	mpcom	$⊢ J \in Fre \to J \in Kol2$