Metamath Proof Explorer

Theorem ist1-3

Description: A space is T_1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion ist1-3 
|- ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. x e. X |^| { o e. J | x e. o } = { x } ) )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
3 eleq2 
 |-  ( o = X -> ( x e. o <-> x e. X ) )
4 3 intminss 
 |-  ( ( X e. J /\ x e. X ) -> |^| { o e. J | x e. o } C_ X )
5 2 4 sylan 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. X ) -> |^| { o e. J | x e. o } C_ X )
6 5 sselda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x e. X ) /\ y e. |^| { o e. J | x e. o } ) -> y e. X )
7 biimt 
 |-  ( y e. X -> ( y e. { x } <-> ( y e. X -> y e. { x } ) ) )
8 6 7 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ x e. X ) /\ y e. |^| { o e. J | x e. o } ) -> ( y e. { x } <-> ( y e. X -> y e. { x } ) ) )
9 8 ralbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. X ) -> ( A. y e. |^| { o e. J | x e. o } y e. { x } <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) ) )
10 id 
 |-  ( x e. o -> x e. o )
11 10 rgenw 
 |-  A. o e. J ( x e. o -> x e. o )
12 vex 
 |-  x e. _V
13 12 elintrab 
 |-  ( x e. |^| { o e. J | x e. o } <-> A. o e. J ( x e. o -> x e. o ) )
14 11 13 mpbir 
 |-  x e. |^| { o e. J | x e. o }
15 snssi 
 |-  ( x e. |^| { o e. J | x e. o } -> { x } C_ |^| { o e. J | x e. o } )
16 14 15 ax-mp 
 |-  { x } C_ |^| { o e. J | x e. o }
17 eqss 
 |-  ( |^| { o e. J | x e. o } = { x } <-> ( |^| { o e. J | x e. o } C_ { x } /\ { x } C_ |^| { o e. J | x e. o } ) )
18 16 17 mpbiran2 
 |-  ( |^| { o e. J | x e. o } = { x } <-> |^| { o e. J | x e. o } C_ { x } )
19 dfss3 
 |-  ( |^| { o e. J | x e. o } C_ { x } <-> A. y e. |^| { o e. J | x e. o } y e. { x } )
20 18 19 bitri 
 |-  ( |^| { o e. J | x e. o } = { x } <-> A. y e. |^| { o e. J | x e. o } y e. { x } )
21 vex 
 |-  y e. _V
22 21 elintrab 
 |-  ( y e. |^| { o e. J | x e. o } <-> A. o e. J ( x e. o -> y e. o ) )
23 velsn 
 |-  ( y e. { x } <-> y = x )
24 equcom 
 |-  ( y = x <-> x = y )
25 23 24 bitri 
 |-  ( y e. { x } <-> x = y )
26 22 25 imbi12i 
 |-  ( ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) )
27 26 ralbii 
 |-  ( A. y e. X ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) )
28 ralcom3 
 |-  ( A. y e. X ( y e. |^| { o e. J | x e. o } -> y e. { x } ) <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) )
29 27 28 bitr3i 
 |-  ( A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. y e. |^| { o e. J | x e. o } ( y e. X -> y e. { x } ) )
30 9 20 29 3bitr4g 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. X ) -> ( |^| { o e. J | x e. o } = { x } <-> A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
31 30 ralbidva 
 |-  ( J e. ( TopOn ` X ) -> ( A. x e. X |^| { o e. J | x e. o } = { x } <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
32 1 31 bitr4d 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. x e. X |^| { o e. J | x e. o } = { x } ) )