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