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

Metamath Proof Explorer

Theorem t0sep

Description: Any two topologically indistinguishable points in a T_0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis ist0.1 
|- X = U. J
Assertion t0sep 
|- ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )

Proof

Step Hyp Ref Expression
1 ist0.1 
 |-  X = U. J
2 1 ist0 
 |-  ( J e. Kol2 <-> ( J e. Top /\ A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) ) )
3 2 simprbi 
 |-  ( J e. Kol2 -> A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) )
4 eleq1 
 |-  ( y = A -> ( y e. x <-> A e. x ) )
5 4 bibi1d 
 |-  ( y = A -> ( ( y e. x <-> z e. x ) <-> ( A e. x <-> z e. x ) ) )
6 5 ralbidv 
 |-  ( y = A -> ( A. x e. J ( y e. x <-> z e. x ) <-> A. x e. J ( A e. x <-> z e. x ) ) )
7 eqeq1 
 |-  ( y = A -> ( y = z <-> A = z ) )
8 6 7 imbi12d 
 |-  ( y = A -> ( ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) <-> ( A. x e. J ( A e. x <-> z e. x ) -> A = z ) ) )
9 eleq1 
 |-  ( z = B -> ( z e. x <-> B e. x ) )
10 9 bibi2d 
 |-  ( z = B -> ( ( A e. x <-> z e. x ) <-> ( A e. x <-> B e. x ) ) )
11 10 ralbidv 
 |-  ( z = B -> ( A. x e. J ( A e. x <-> z e. x ) <-> A. x e. J ( A e. x <-> B e. x ) ) )
12 eqeq2 
 |-  ( z = B -> ( A = z <-> A = B ) )
13 11 12 imbi12d 
 |-  ( z = B -> ( ( A. x e. J ( A e. x <-> z e. x ) -> A = z ) <-> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) ) )
14 8 13 rspc2va 
 |-  ( ( ( A e. X /\ B e. X ) /\ A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )
15 14 ancoms 
 |-  ( ( A. y e. X A. z e. X ( A. x e. J ( y e. x <-> z e. x ) -> y = z ) /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )
16 3 15 sylan 
 |-  ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )