Metamath Proof Explorer

Theorem ist1-2

Description: An alternate characterization of T_1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 eqid 
 |-  U. J = U. J
3 2 ist1 
 |-  ( J e. Fre <-> ( J e. Top /\ A. y e. U. J { y } e. ( Clsd ` J ) ) )
4 3 baib 
 |-  ( J e. Top -> ( J e. Fre <-> A. y e. U. J { y } e. ( Clsd ` J ) ) )
5 1 4 syl 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Fre <-> A. y e. U. J { y } e. ( Clsd ` J ) ) )
6 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
7 6 raleqdv 
 |-  ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. y e. U. J { y } e. ( Clsd ` J ) ) )
8 1 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> J e. Top )
9 eltop2 
 |-  ( J e. Top -> ( ( U. J \ { y } ) e. J <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
10 8 9 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( U. J \ { y } ) e. J <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
11 6 eleq2d 
 |-  ( J e. ( TopOn ` X ) -> ( y e. X <-> y e. U. J ) )
12 11 biimpa 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> y e. U. J )
13 12 snssd 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> { y } C_ U. J )
14 2 iscld2 
 |-  ( ( J e. Top /\ { y } C_ U. J ) -> ( { y } e. ( Clsd ` J ) <-> ( U. J \ { y } ) e. J ) )
15 8 13 14 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( { y } e. ( Clsd ` J ) <-> ( U. J \ { y } ) e. J ) )
16 6 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> X = U. J )
17 16 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( x e. X <-> x e. U. J ) )
18 17 imbi1d 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( x e. X -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) ) )
19 con1b 
 |-  ( ( -. x = y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) -> x = y ) )
20 df-ne 
 |-  ( x =/= y <-> -. x = y )
21 20 imbi1i 
 |-  ( ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( -. x = y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
22 disjsn 
 |-  ( ( o i^i { y } ) = (/) <-> -. y e. o )
23 elssuni 
 |-  ( o e. J -> o C_ U. J )
24 reldisj 
 |-  ( o C_ U. J -> ( ( o i^i { y } ) = (/) <-> o C_ ( U. J \ { y } ) ) )
25 23 24 syl 
 |-  ( o e. J -> ( ( o i^i { y } ) = (/) <-> o C_ ( U. J \ { y } ) ) )
26 22 25 bitr3id 
 |-  ( o e. J -> ( -. y e. o <-> o C_ ( U. J \ { y } ) ) )
27 26 anbi2d 
 |-  ( o e. J -> ( ( x e. o /\ -. y e. o ) <-> ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
28 27 rexbiia 
 |-  ( E. o e. J ( x e. o /\ -. y e. o ) <-> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) )
29 rexanali 
 |-  ( E. o e. J ( x e. o /\ -. y e. o ) <-> -. A. o e. J ( x e. o -> y e. o ) )
30 28 29 bitr3i 
 |-  ( E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) <-> -. A. o e. J ( x e. o -> y e. o ) )
31 30 con2bii 
 |-  ( A. o e. J ( x e. o -> y e. o ) <-> -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) )
32 31 imbi1i 
 |-  ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> ( -. E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) -> x = y ) )
33 19 21 32 3bitr4ri 
 |-  ( ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
34 33 imbi2i 
 |-  ( ( x e. X -> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) <-> ( x e. X -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) )
35 eldifsn 
 |-  ( x e. ( U. J \ { y } ) <-> ( x e. U. J /\ x =/= y ) )
36 35 imbi1i 
 |-  ( ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( ( x e. U. J /\ x =/= y ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
37 impexp 
 |-  ( ( ( x e. U. J /\ x =/= y ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) )
38 36 37 bitri 
 |-  ( ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) <-> ( x e. U. J -> ( x =/= y -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) )
39 18 34 38 3bitr4g 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( ( x e. X -> ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) <-> ( x e. ( U. J \ { y } ) -> E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) ) )
40 39 ralbidv2 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. x e. ( U. J \ { y } ) E. o e. J ( x e. o /\ o C_ ( U. J \ { y } ) ) ) )
41 10 15 40 3bitr4d 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. X ) -> ( { y } e. ( Clsd ` J ) <-> A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
42 41 ralbidva 
 |-  ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. y e. X A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
43 ralcom 
 |-  ( A. y e. X A. x e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) )
44 42 43 bitrdi 
 |-  ( J e. ( TopOn ` X ) -> ( A. y e. X { y } e. ( Clsd ` J ) <-> A. x e. X A. y e. X ( A. o e. J ( x e. o -> y e. o ) -> x = y ) ) )
45 5 7 44 3bitr2d 
 |-  ( 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 ) ) )