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