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

Metamath Proof Explorer

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 ) )