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 φ B = J
ist0cls.2 φ D = Clsd J
Assertion ist0cld φ J Kol2 J Top x B y B d D x d y d x = y

Proof

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