Step | Hyp | Ref
| Expression |
1 | | unieq 4881 |
. . . . . . . . 9
β’ (π = β
β βͺ π =
βͺ β
) |
2 | | uni0 4901 |
. . . . . . . . 9
β’ βͺ β
= β
|
3 | 1, 2 | eqtrdi 2793 |
. . . . . . . 8
β’ (π = β
β βͺ π =
β
) |
4 | 3 | eleq1d 2823 |
. . . . . . 7
β’ (π = β
β (βͺ π
β π½ β β
β π½)) |
5 | | mretopd.j |
. . . . . . . . . . . . . 14
β’ π½ = {π§ β π« π΅ β£ (π΅ β π§) β π} |
6 | 5 | ssrab3 4045 |
. . . . . . . . . . . . 13
β’ π½ β π« π΅ |
7 | | sstr 3957 |
. . . . . . . . . . . . 13
β’ ((π β π½ β§ π½ β π« π΅) β π β π« π΅) |
8 | 6, 7 | mpan2 690 |
. . . . . . . . . . . 12
β’ (π β π½ β π β π« π΅) |
9 | 8 | adantl 483 |
. . . . . . . . . . 11
β’ ((π β§ π β π½) β π β π« π΅) |
10 | | sspwuni 5065 |
. . . . . . . . . . 11
β’ (π β π« π΅ β βͺ π
β π΅) |
11 | 9, 10 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β π½) β βͺ π β π΅) |
12 | | vuniex 7681 |
. . . . . . . . . . 11
β’ βͺ π
β V |
13 | 12 | elpw 4569 |
. . . . . . . . . 10
β’ (βͺ π
β π« π΅ β
βͺ π β π΅) |
14 | 11, 13 | sylibr 233 |
. . . . . . . . 9
β’ ((π β§ π β π½) β βͺ π β π« π΅) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β π½) β§ π β β
) β βͺ π
β π« π΅) |
16 | | uniiun 5023 |
. . . . . . . . . 10
β’ βͺ π =
βͺ π β π π |
17 | 16 | difeq2i 4084 |
. . . . . . . . 9
β’ (π΅ β βͺ π) =
(π΅ β βͺ π β π π) |
18 | | iindif2 5042 |
. . . . . . . . . . 11
β’ (π β β
β β© π β π (π΅ β π) = (π΅ β βͺ
π β π π)) |
19 | 18 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ π β π½) β§ π β β
) β β© π β π (π΅ β π) = (π΅ β βͺ
π β π π)) |
20 | | mretopd.m |
. . . . . . . . . . . 12
β’ (π β π β (Mooreβπ΅)) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β π½) β§ π β β
) β π β (Mooreβπ΅)) |
22 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β π½) β§ π β β
) β π β β
) |
23 | | difeq2 4081 |
. . . . . . . . . . . . . . . . 17
β’ (π§ = π β (π΅ β π§) = (π΅ β π)) |
24 | 23 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π§ = π β ((π΅ β π§) β π β (π΅ β π) β π)) |
25 | 24, 5 | elrab2 3653 |
. . . . . . . . . . . . . . 15
β’ (π β π½ β (π β π« π΅ β§ (π΅ β π) β π)) |
26 | 25 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π β π½ β (π΅ β π) β π) |
27 | 26 | rgen 3067 |
. . . . . . . . . . . . 13
β’
βπ β
π½ (π΅ β π) β π |
28 | | ssralv 4015 |
. . . . . . . . . . . . . 14
β’ (π β π½ β (βπ β π½ (π΅ β π) β π β βπ β π (π΅ β π) β π)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π½) β (βπ β π½ (π΅ β π) β π β βπ β π (π΅ β π) β π)) |
30 | 27, 29 | mpi 20 |
. . . . . . . . . . . 12
β’ ((π β§ π β π½) β βπ β π (π΅ β π) β π) |
31 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π½) β§ π β β
) β βπ β π (π΅ β π) β π) |
32 | | mreiincl 17483 |
. . . . . . . . . . 11
β’ ((π β (Mooreβπ΅) β§ π β β
β§ βπ β π (π΅ β π) β π) β β©
π β π (π΅ β π) β π) |
33 | 21, 22, 31, 32 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β π½) β§ π β β
) β β© π β π (π΅ β π) β π) |
34 | 19, 33 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ π β π½) β§ π β β
) β (π΅ β βͺ
π β π π) β π) |
35 | 17, 34 | eqeltrid 2842 |
. . . . . . . 8
β’ (((π β§ π β π½) β§ π β β
) β (π΅ β βͺ π) β π) |
36 | | difeq2 4081 |
. . . . . . . . . 10
β’ (π§ = βͺ
π β (π΅ β π§) = (π΅ β βͺ π)) |
37 | 36 | eleq1d 2823 |
. . . . . . . . 9
β’ (π§ = βͺ
π β ((π΅ β π§) β π β (π΅ β βͺ π) β π)) |
38 | 37, 5 | elrab2 3653 |
. . . . . . . 8
β’ (βͺ π
β π½ β (βͺ π
β π« π΅ β§
(π΅ β βͺ π)
β π)) |
39 | 15, 35, 38 | sylanbrc 584 |
. . . . . . 7
β’ (((π β§ π β π½) β§ π β β
) β βͺ π
β π½) |
40 | | 0elpw 5316 |
. . . . . . . . . 10
β’ β
β π« π΅ |
41 | 40 | a1i 11 |
. . . . . . . . 9
β’ (π β β
β π«
π΅) |
42 | | mre1cl 17481 |
. . . . . . . . . 10
β’ (π β (Mooreβπ΅) β π΅ β π) |
43 | 20, 42 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β π) |
44 | | difeq2 4081 |
. . . . . . . . . . . 12
β’ (π§ = β
β (π΅ β π§) = (π΅ β β
)) |
45 | | dif0 4337 |
. . . . . . . . . . . 12
β’ (π΅ β β
) = π΅ |
46 | 44, 45 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (π§ = β
β (π΅ β π§) = π΅) |
47 | 46 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π§ = β
β ((π΅ β π§) β π β π΅ β π)) |
48 | 47, 5 | elrab2 3653 |
. . . . . . . . 9
β’ (β
β π½ β (β
β π« π΅ β§
π΅ β π)) |
49 | 41, 43, 48 | sylanbrc 584 |
. . . . . . . 8
β’ (π β β
β π½) |
50 | 49 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π½) β β
β π½) |
51 | 4, 39, 50 | pm2.61ne 3031 |
. . . . . 6
β’ ((π β§ π β π½) β βͺ π β π½) |
52 | 51 | ex 414 |
. . . . 5
β’ (π β (π β π½ β βͺ π β π½)) |
53 | 52 | alrimiv 1931 |
. . . 4
β’ (π β βπ(π β π½ β βͺ π β π½)) |
54 | | inss1 4193 |
. . . . . . . 8
β’ (π β© π) β π |
55 | | difeq2 4081 |
. . . . . . . . . . . . 13
β’ (π§ = π β (π΅ β π§) = (π΅ β π)) |
56 | 55 | eleq1d 2823 |
. . . . . . . . . . . 12
β’ (π§ = π β ((π΅ β π§) β π β (π΅ β π) β π)) |
57 | 56, 5 | elrab2 3653 |
. . . . . . . . . . 11
β’ (π β π½ β (π β π« π΅ β§ (π΅ β π) β π)) |
58 | 57 | simplbi 499 |
. . . . . . . . . 10
β’ (π β π½ β π β π« π΅) |
59 | 58 | elpwid 4574 |
. . . . . . . . 9
β’ (π β π½ β π β π΅) |
60 | 59 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β π½ β§ π β π½)) β π β π΅) |
61 | 54, 60 | sstrid 3960 |
. . . . . . 7
β’ ((π β§ (π β π½ β§ π β π½)) β (π β© π) β π΅) |
62 | | vex 3452 |
. . . . . . . . 9
β’ π β V |
63 | 62 | inex1 5279 |
. . . . . . . 8
β’ (π β© π) β V |
64 | 63 | elpw 4569 |
. . . . . . 7
β’ ((π β© π) β π« π΅ β (π β© π) β π΅) |
65 | 61, 64 | sylibr 233 |
. . . . . 6
β’ ((π β§ (π β π½ β§ π β π½)) β (π β© π) β π« π΅) |
66 | | difindi 4246 |
. . . . . . 7
β’ (π΅ β (π β© π)) = ((π΅ β π) βͺ (π΅ β π)) |
67 | 57 | simprbi 498 |
. . . . . . . . 9
β’ (π β π½ β (π΅ β π) β π) |
68 | 67 | ad2antrl 727 |
. . . . . . . 8
β’ ((π β§ (π β π½ β§ π β π½)) β (π΅ β π) β π) |
69 | 26 | ad2antll 728 |
. . . . . . . 8
β’ ((π β§ (π β π½ β§ π β π½)) β (π΅ β π) β π) |
70 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ (π β π½ β§ π β π½)) β π) |
71 | | uneq1 4121 |
. . . . . . . . . . . 12
β’ (π₯ = (π΅ β π) β (π₯ βͺ π¦) = ((π΅ β π) βͺ π¦)) |
72 | 71 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π₯ = (π΅ β π) β ((π₯ βͺ π¦) β π β ((π΅ β π) βͺ π¦) β π)) |
73 | 72 | imbi2d 341 |
. . . . . . . . . 10
β’ (π₯ = (π΅ β π) β ((π β (π₯ βͺ π¦) β π) β (π β ((π΅ β π) βͺ π¦) β π))) |
74 | | uneq2 4122 |
. . . . . . . . . . . 12
β’ (π¦ = (π΅ β π) β ((π΅ β π) βͺ π¦) = ((π΅ β π) βͺ (π΅ β π))) |
75 | 74 | eleq1d 2823 |
. . . . . . . . . . 11
β’ (π¦ = (π΅ β π) β (((π΅ β π) βͺ π¦) β π β ((π΅ β π) βͺ (π΅ β π)) β π)) |
76 | 75 | imbi2d 341 |
. . . . . . . . . 10
β’ (π¦ = (π΅ β π) β ((π β ((π΅ β π) βͺ π¦) β π) β (π β ((π΅ β π) βͺ (π΅ β π)) β π))) |
77 | | mretopd.u |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ βͺ π¦) β π) |
78 | 77 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ βͺ π¦) β π) |
79 | 78 | expcom 415 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π¦ β π) β (π β (π₯ βͺ π¦) β π)) |
80 | 73, 76, 79 | vtocl2ga 3538 |
. . . . . . . . 9
β’ (((π΅ β π) β π β§ (π΅ β π) β π) β (π β ((π΅ β π) βͺ (π΅ β π)) β π)) |
81 | 80 | imp 408 |
. . . . . . . 8
β’ ((((π΅ β π) β π β§ (π΅ β π) β π) β§ π) β ((π΅ β π) βͺ (π΅ β π)) β π) |
82 | 68, 69, 70, 81 | syl21anc 837 |
. . . . . . 7
β’ ((π β§ (π β π½ β§ π β π½)) β ((π΅ β π) βͺ (π΅ β π)) β π) |
83 | 66, 82 | eqeltrid 2842 |
. . . . . 6
β’ ((π β§ (π β π½ β§ π β π½)) β (π΅ β (π β© π)) β π) |
84 | | difeq2 4081 |
. . . . . . . 8
β’ (π§ = (π β© π) β (π΅ β π§) = (π΅ β (π β© π))) |
85 | 84 | eleq1d 2823 |
. . . . . . 7
β’ (π§ = (π β© π) β ((π΅ β π§) β π β (π΅ β (π β© π)) β π)) |
86 | 85, 5 | elrab2 3653 |
. . . . . 6
β’ ((π β© π) β π½ β ((π β© π) β π« π΅ β§ (π΅ β (π β© π)) β π)) |
87 | 65, 83, 86 | sylanbrc 584 |
. . . . 5
β’ ((π β§ (π β π½ β§ π β π½)) β (π β© π) β π½) |
88 | 87 | ralrimivva 3198 |
. . . 4
β’ (π β βπ β π½ βπ β π½ (π β© π) β π½) |
89 | 43 | pwexd 5339 |
. . . . . 6
β’ (π β π« π΅ β V) |
90 | 5, 89 | rabexd 5295 |
. . . . 5
β’ (π β π½ β V) |
91 | | istopg 22260 |
. . . . 5
β’ (π½ β V β (π½ β Top β
(βπ(π β π½ β βͺ π β π½) β§ βπ β π½ βπ β π½ (π β© π) β π½))) |
92 | 90, 91 | syl 17 |
. . . 4
β’ (π β (π½ β Top β (βπ(π β π½ β βͺ π β π½) β§ βπ β π½ βπ β π½ (π β© π) β π½))) |
93 | 53, 88, 92 | mpbir2and 712 |
. . 3
β’ (π β π½ β Top) |
94 | 6 | unissi 4879 |
. . . . . 6
β’ βͺ π½
β βͺ π« π΅ |
95 | | unipw 5412 |
. . . . . 6
β’ βͺ π« π΅ = π΅ |
96 | 94, 95 | sseqtri 3985 |
. . . . 5
β’ βͺ π½
β π΅ |
97 | | pwidg 4585 |
. . . . . . 7
β’ (π΅ β π β π΅ β π« π΅) |
98 | 43, 97 | syl 17 |
. . . . . 6
β’ (π β π΅ β π« π΅) |
99 | | difid 4335 |
. . . . . . 7
β’ (π΅ β π΅) = β
|
100 | | mretopd.z |
. . . . . . 7
β’ (π β β
β π) |
101 | 99, 100 | eqeltrid 2842 |
. . . . . 6
β’ (π β (π΅ β π΅) β π) |
102 | | difeq2 4081 |
. . . . . . . 8
β’ (π§ = π΅ β (π΅ β π§) = (π΅ β π΅)) |
103 | 102 | eleq1d 2823 |
. . . . . . 7
β’ (π§ = π΅ β ((π΅ β π§) β π β (π΅ β π΅) β π)) |
104 | 103, 5 | elrab2 3653 |
. . . . . 6
β’ (π΅ β π½ β (π΅ β π« π΅ β§ (π΅ β π΅) β π)) |
105 | 98, 101, 104 | sylanbrc 584 |
. . . . 5
β’ (π β π΅ β π½) |
106 | | unissel 4904 |
. . . . 5
β’ ((βͺ π½
β π΅ β§ π΅ β π½) β βͺ π½ = π΅) |
107 | 96, 105, 106 | sylancr 588 |
. . . 4
β’ (π β βͺ π½ =
π΅) |
108 | 107 | eqcomd 2743 |
. . 3
β’ (π β π΅ = βͺ π½) |
109 | | istopon 22277 |
. . 3
β’ (π½ β (TopOnβπ΅) β (π½ β Top β§ π΅ = βͺ π½)) |
110 | 93, 108, 109 | sylanbrc 584 |
. 2
β’ (π β π½ β (TopOnβπ΅)) |
111 | | eqid 2737 |
. . . . 5
β’ βͺ π½ =
βͺ π½ |
112 | 111 | cldval 22390 |
. . . 4
β’ (π½ β Top β
(Clsdβπ½) = {π₯ β π« βͺ π½
β£ (βͺ π½ β π₯) β π½}) |
113 | 93, 112 | syl 17 |
. . 3
β’ (π β (Clsdβπ½) = {π₯ β π« βͺ π½
β£ (βͺ π½ β π₯) β π½}) |
114 | 107 | pweqd 4582 |
. . . 4
β’ (π β π« βͺ π½ =
π« π΅) |
115 | 107 | difeq1d 4086 |
. . . . 5
β’ (π β (βͺ π½
β π₯) = (π΅ β π₯)) |
116 | 115 | eleq1d 2823 |
. . . 4
β’ (π β ((βͺ π½
β π₯) β π½ β (π΅ β π₯) β π½)) |
117 | 114, 116 | rabeqbidv 3427 |
. . 3
β’ (π β {π₯ β π« βͺ π½
β£ (βͺ π½ β π₯) β π½} = {π₯ β π« π΅ β£ (π΅ β π₯) β π½}) |
118 | 5 | eleq2i 2830 |
. . . . . . 7
β’ ((π΅ β π₯) β π½ β (π΅ β π₯) β {π§ β π« π΅ β£ (π΅ β π§) β π}) |
119 | | difss 4096 |
. . . . . . . . . 10
β’ (π΅ β π₯) β π΅ |
120 | | elpw2g 5306 |
. . . . . . . . . . 11
β’ (π΅ β π β ((π΅ β π₯) β π« π΅ β (π΅ β π₯) β π΅)) |
121 | 43, 120 | syl 17 |
. . . . . . . . . 10
β’ (π β ((π΅ β π₯) β π« π΅ β (π΅ β π₯) β π΅)) |
122 | 119, 121 | mpbiri 258 |
. . . . . . . . 9
β’ (π β (π΅ β π₯) β π« π΅) |
123 | | difeq2 4081 |
. . . . . . . . . . 11
β’ (π§ = (π΅ β π₯) β (π΅ β π§) = (π΅ β (π΅ β π₯))) |
124 | 123 | eleq1d 2823 |
. . . . . . . . . 10
β’ (π§ = (π΅ β π₯) β ((π΅ β π§) β π β (π΅ β (π΅ β π₯)) β π)) |
125 | 124 | elrab3 3651 |
. . . . . . . . 9
β’ ((π΅ β π₯) β π« π΅ β ((π΅ β π₯) β {π§ β π« π΅ β£ (π΅ β π§) β π} β (π΅ β (π΅ β π₯)) β π)) |
126 | 122, 125 | syl 17 |
. . . . . . . 8
β’ (π β ((π΅ β π₯) β {π§ β π« π΅ β£ (π΅ β π§) β π} β (π΅ β (π΅ β π₯)) β π)) |
127 | 126 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β π« π΅) β ((π΅ β π₯) β {π§ β π« π΅ β£ (π΅ β π§) β π} β (π΅ β (π΅ β π₯)) β π)) |
128 | 118, 127 | bitrid 283 |
. . . . . 6
β’ ((π β§ π₯ β π« π΅) β ((π΅ β π₯) β π½ β (π΅ β (π΅ β π₯)) β π)) |
129 | | elpwi 4572 |
. . . . . . . . 9
β’ (π₯ β π« π΅ β π₯ β π΅) |
130 | | dfss4 4223 |
. . . . . . . . 9
β’ (π₯ β π΅ β (π΅ β (π΅ β π₯)) = π₯) |
131 | 129, 130 | sylib 217 |
. . . . . . . 8
β’ (π₯ β π« π΅ β (π΅ β (π΅ β π₯)) = π₯) |
132 | 131 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β π« π΅) β (π΅ β (π΅ β π₯)) = π₯) |
133 | 132 | eleq1d 2823 |
. . . . . 6
β’ ((π β§ π₯ β π« π΅) β ((π΅ β (π΅ β π₯)) β π β π₯ β π)) |
134 | 128, 133 | bitrd 279 |
. . . . 5
β’ ((π β§ π₯ β π« π΅) β ((π΅ β π₯) β π½ β π₯ β π)) |
135 | 134 | rabbidva 3417 |
. . . 4
β’ (π β {π₯ β π« π΅ β£ (π΅ β π₯) β π½} = {π₯ β π« π΅ β£ π₯ β π}) |
136 | | incom 4166 |
. . . . . 6
β’ (π β© π« π΅) = (π« π΅ β© π) |
137 | | dfin5 3923 |
. . . . . 6
β’
(π« π΅ β©
π) = {π₯ β π« π΅ β£ π₯ β π} |
138 | 136, 137 | eqtri 2765 |
. . . . 5
β’ (π β© π« π΅) = {π₯ β π« π΅ β£ π₯ β π} |
139 | | mresspw 17479 |
. . . . . . 7
β’ (π β (Mooreβπ΅) β π β π« π΅) |
140 | 20, 139 | syl 17 |
. . . . . 6
β’ (π β π β π« π΅) |
141 | | df-ss 3932 |
. . . . . 6
β’ (π β π« π΅ β (π β© π« π΅) = π) |
142 | 140, 141 | sylib 217 |
. . . . 5
β’ (π β (π β© π« π΅) = π) |
143 | 138, 142 | eqtr3id 2791 |
. . . 4
β’ (π β {π₯ β π« π΅ β£ π₯ β π} = π) |
144 | 135, 143 | eqtrd 2777 |
. . 3
β’ (π β {π₯ β π« π΅ β£ (π΅ β π₯) β π½} = π) |
145 | 113, 117,
144 | 3eqtrrd 2782 |
. 2
β’ (π β π = (Clsdβπ½)) |
146 | 110, 145 | jca 513 |
1
β’ (π β (π½ β (TopOnβπ΅) β§ π = (Clsdβπ½))) |