Metamath Proof Explorer

Theorem ist0cld

Description: The predicate "is a T_0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020)

Ref Expression
Hypotheses ist0cls.1 
|- ( ph -> B = U. J )
ist0cls.2 
|- ( ph -> D = ( Clsd ` J ) )
Assertion ist0cld 
|- ( ph -> ( J e. Kol2 <-> ( J e. Top /\ A. x e. B A. y e. B ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) ) )

Proof

Step Hyp Ref Expression
1 ist0cls.1 
 |-  ( ph -> B = U. J )
2 ist0cls.2 
 |-  ( ph -> D = ( Clsd ` J ) )
3 eqid 
 |-  U. J = U. J
4 3 ist0 
 |-  ( J e. Kol2 <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
5 4 simplbi 
 |-  ( J e. Kol2 -> J e. Top )
6 5 adantl 
 |-  ( ( ph /\ J e. Kol2 ) -> J e. Top )
7 4 baib 
 |-  ( J e. Top -> ( J e. Kol2 <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
8 7 adantl 
 |-  ( ( ph /\ J e. Top ) -> ( J e. Kol2 <-> A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
9 1 adantr 
 |-  ( ( ph /\ J e. Top ) -> B = U. J )
10 9 eqcomd 
 |-  ( ( ph /\ J e. Top ) -> U. J = B )
11 10 adantr 
 |-  ( ( ( ph /\ J e. Top ) /\ x e. U. J ) -> U. J = B )
12 simp-4r 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ o e. J ) -> J e. Top )
13 uniexg 
 |-  ( J e. Top -> U. J e. _V )
14 difexg 
 |-  ( U. J e. _V -> ( U. J \ o ) e. _V )
15 12 13 14 3syl 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ o e. J ) -> ( U. J \ o ) e. _V )
16 3 iscld 
 |-  ( J e. Top -> ( d e. ( Clsd ` J ) <-> ( d C_ U. J /\ ( U. J \ d ) e. J ) ) )
17 16 adantl 
 |-  ( ( ph /\ J e. Top ) -> ( d e. ( Clsd ` J ) <-> ( d C_ U. J /\ ( U. J \ d ) e. J ) ) )
18 2 eleq2d 
 |-  ( ph -> ( d e. D <-> d e. ( Clsd ` J ) ) )
19 18 adantr 
 |-  ( ( ph /\ J e. Top ) -> ( d e. D <-> d e. ( Clsd ` J ) ) )
20 simpr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> d = ( U. J \ o ) )
21 difssd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> ( U. J \ o ) C_ U. J )
22 20 21 eqsstrd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> d C_ U. J )
23 22 r19.29an 
 |-  ( ( ( ph /\ J e. Top ) /\ E. o e. J d = ( U. J \ o ) ) -> d C_ U. J )
24 simpr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> d = ( U. J \ o ) )
25 24 difeq2d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> ( U. J \ d ) = ( U. J \ ( U. J \ o ) ) )
26 3 eltopss 
 |-  ( ( J e. Top /\ o e. J ) -> o C_ U. J )
27 26 ad5ant24 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> o C_ U. J )
28 dfss4 
 |-  ( o C_ U. J <-> ( U. J \ ( U. J \ o ) ) = o )
29 27 28 sylib 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> ( U. J \ ( U. J \ o ) ) = o )
30 simplr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> o e. J )
31 29 30 eqeltrd 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> ( U. J \ ( U. J \ o ) ) e. J )
32 25 31 eqeltrd 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ o e. J ) /\ d = ( U. J \ o ) ) -> ( U. J \ d ) e. J )
33 32 r19.29an 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ E. o e. J d = ( U. J \ o ) ) -> ( U. J \ d ) e. J )
34 simpr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) -> ( U. J \ d ) e. J )
35 simpr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) /\ o = ( U. J \ d ) ) -> o = ( U. J \ d ) )
36 35 difeq2d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) /\ o = ( U. J \ d ) ) -> ( U. J \ o ) = ( U. J \ ( U. J \ d ) ) )
37 36 eqeq2d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) /\ o = ( U. J \ d ) ) -> ( d = ( U. J \ o ) <-> d = ( U. J \ ( U. J \ d ) ) ) )
38 simplr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) -> d C_ U. J )
39 dfss4 
 |-  ( d C_ U. J <-> ( U. J \ ( U. J \ d ) ) = d )
40 38 39 sylib 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) -> ( U. J \ ( U. J \ d ) ) = d )
41 40 eqcomd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) -> d = ( U. J \ ( U. J \ d ) ) )
42 34 37 41 rspcedvd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) /\ ( U. J \ d ) e. J ) -> E. o e. J d = ( U. J \ o ) )
43 33 42 impbida 
 |-  ( ( ( ph /\ J e. Top ) /\ d C_ U. J ) -> ( E. o e. J d = ( U. J \ o ) <-> ( U. J \ d ) e. J ) )
44 23 43 biadanid 
 |-  ( ( ph /\ J e. Top ) -> ( E. o e. J d = ( U. J \ o ) <-> ( d C_ U. J /\ ( U. J \ d ) e. J ) ) )
45 17 19 44 3bitr4d 
 |-  ( ( ph /\ J e. Top ) -> ( d e. D <-> E. o e. J d = ( U. J \ o ) ) )
46 45 ad2antrr 
 |-  ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) -> ( d e. D <-> E. o e. J d = ( U. J \ o ) ) )
47 simpr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> d = ( U. J \ o ) )
48 47 eleq2d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( x e. d <-> x e. ( U. J \ o ) ) )
49 eldif 
 |-  ( x e. ( U. J \ o ) <-> ( x e. U. J /\ -. x e. o ) )
50 49 baib 
 |-  ( x e. U. J -> ( x e. ( U. J \ o ) <-> -. x e. o ) )
51 50 ad3antlr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( x e. ( U. J \ o ) <-> -. x e. o ) )
52 48 51 bitrd 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( x e. d <-> -. x e. o ) )
53 47 eleq2d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( y e. d <-> y e. ( U. J \ o ) ) )
54 eldif 
 |-  ( y e. ( U. J \ o ) <-> ( y e. U. J /\ -. y e. o ) )
55 54 baib 
 |-  ( y e. U. J -> ( y e. ( U. J \ o ) <-> -. y e. o ) )
56 55 ad2antlr 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( y e. ( U. J \ o ) <-> -. y e. o ) )
57 53 56 bitrd 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( y e. d <-> -. y e. o ) )
58 52 57 bibi12d 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( ( x e. d <-> y e. d ) <-> ( -. x e. o <-> -. y e. o ) ) )
59 notbi 
 |-  ( ( x e. o <-> y e. o ) <-> ( -. x e. o <-> -. y e. o ) )
60 58 59 bitr4di 
 |-  ( ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) /\ d = ( U. J \ o ) ) -> ( ( x e. d <-> y e. d ) <-> ( x e. o <-> y e. o ) ) )
61 15 46 60 ralxfr2d 
 |-  ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) -> ( A. d e. D ( x e. d <-> y e. d ) <-> A. o e. J ( x e. o <-> y e. o ) ) )
62 61 bicomd 
 |-  ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) -> ( A. o e. J ( x e. o <-> y e. o ) <-> A. d e. D ( x e. d <-> y e. d ) ) )
63 62 imbi1d 
 |-  ( ( ( ( ph /\ J e. Top ) /\ x e. U. J ) /\ y e. U. J ) -> ( ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) )
64 11 63 raleqbidva 
 |-  ( ( ( ph /\ J e. Top ) /\ x e. U. J ) -> ( A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> A. y e. B ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) )
65 10 64 raleqbidva 
 |-  ( ( ph /\ J e. Top ) -> ( A. x e. U. J A. y e. U. J ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) <-> A. x e. B A. y e. B ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) )
66 8 65 bitrd 
 |-  ( ( ph /\ J e. Top ) -> ( J e. Kol2 <-> A. x e. B A. y e. B ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) )
67 6 66 biadanid 
 |-  ( ph -> ( J e. Kol2 <-> ( J e. Top /\ A. x e. B A. y e. B ( A. d e. D ( x e. d <-> y e. d ) -> x = y ) ) ) )