Theorem t1sep2

Description: Any two points in a T_1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010)

	Ref	Expression
Hypothesis	t1sep.1	|- X = U. J
Assertion	t1sep2	|- ( ( J e. Fre /\ A e. X /\ B e. X ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		t1sep.1	|- X = U. J
2		t1top	|- ( J e. Fre -> J e. Top )
3	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
4	2 3	sylib	|- ( J e. Fre -> J e. ( TopOn ` X ) )
5		ist1-2	|- ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
6	4 5	syl	|- ( J e. Fre -> ( J e. Fre <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
7	6	ibi	|- ( J e. Fre -> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) )
8		eleq1	|- ( x = A -> ( x e. o <-> A e. o ) )
9	8	imbi1d	|- ( x = A -> ( ( x e. o -> y e. o ) <-> ( A e. o -> y e. o ) ) )
10	9	ralbidv	|- ( x = A -> ( A. o e. J ( x e. o -> y e. o ) <-> A. o e. J ( A e. o -> y e. o ) ) )
11		eqeq1	|- ( x = A -> ( x = y <-> A = y ) )
12	10 11	imbi12d	|- ( x = A -> ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> ( A. o e. J ( A e. o -> y e. o ) -> A = y ) ) )
13		eleq1	|- ( y = B -> ( y e. o <-> B e. o ) )
14	13	imbi2d	|- ( y = B -> ( ( A e. o -> y e. o ) <-> ( A e. o -> B e. o ) ) )
15	14	ralbidv	|- ( y = B -> ( A. o e. J ( A e. o -> y e. o ) <-> A. o e. J ( A e. o -> B e. o ) ) )
16		eqeq2	|- ( y = B -> ( A = y <-> A = B ) )
17	15 16	imbi12d	|- ( y = B -> ( ( A. o e. J ( A e. o -> y e. o ) -> A = y ) <-> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) ) )
18	12 17	rspc2v	|- ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) ) )
19	7 18	mpan9	|- ( ( J e. Fre /\ ( A e. X /\ B e. X ) ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) )
20	19	3impb	|- ( ( J e. Fre /\ A e. X /\ B e. X ) -> ( A. o e. J ( A e. o -> B e. o ) -> A = B ) )