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

Metamath Proof Explorer

Theorem ist0-3

Description: The predicate "is a T_0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010)

		Ref	Expression
	Assertion	ist0-3	\|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. x e. X A. y e. X ( x =/= y -> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ist0-2	\|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
2		con34b	\|- ( ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> ( -. x = y -> -. A. o e. J ( x e. o <-> y e. o ) ) )
3		df-ne	\|- ( x =/= y <-> -. x = y )
4		xor	\|- ( -. ( x e. o <-> y e. o ) <-> ( ( x e. o /\ -. y e. o ) \/ ( y e. o /\ -. x e. o ) ) )
5		ancom	\|- ( ( y e. o /\ -. x e. o ) <-> ( -. x e. o /\ y e. o ) )
6	5	orbi2i	\|- ( ( ( x e. o /\ -. y e. o ) \/ ( y e. o /\ -. x e. o ) ) <-> ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) )
7	4 6	bitri	\|- ( -. ( x e. o <-> y e. o ) <-> ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) )
8	7	rexbii	\|- ( E. o e. J -. ( x e. o <-> y e. o ) <-> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) )
9		rexnal	\|- ( E. o e. J -. ( x e. o <-> y e. o ) <-> -. A. o e. J ( x e. o <-> y e. o ) )
10	8 9	bitr3i	\|- ( E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) <-> -. A. o e. J ( x e. o <-> y e. o ) )
11	3 10	imbi12i	\|- ( ( x =/= y -> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) ) <-> ( -. x = y -> -. A. o e. J ( x e. o <-> y e. o ) ) )
12	2 11	bitr4i	\|- ( ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> ( x =/= y -> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) ) )
13	12	2ralbii	\|- ( A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> A. x e. X A. y e. X ( x =/= y -> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) ) )
14	1 13	bitrdi	\|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. x e. X A. y e. X ( x =/= y -> E. o e. J ( ( x e. o /\ -. y e. o ) \/ ( -. x e. o /\ y e. o ) ) ) ) )