Step | Hyp | Ref
| Expression |
1 | | nllytop 22847 |
. . 3
β’ (π½ β π-Locally Comp
β π½ β
Top) |
2 | | resttop 22534 |
. . 3
β’ ((π½ β Top β§ π΄ β (Clsdβπ½)) β (π½ βΎt π΄) β Top) |
3 | 1, 2 | sylan 581 |
. 2
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
(π½ βΎt
π΄) β
Top) |
4 | | elrest 17317 |
. . . 4
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
(π₯ β (π½ βΎt π΄) β βπ’ β π½ π₯ = (π’ β© π΄))) |
5 | | simpll 766 |
. . . . . . . . . 10
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β π½ β π-Locally
Comp) |
6 | | simprl 770 |
. . . . . . . . . 10
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β π’ β π½) |
7 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β π¦ β (π’ β© π΄)) |
8 | 7 | elin1d 4162 |
. . . . . . . . . 10
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β π¦ β π’) |
9 | | nlly2i 22850 |
. . . . . . . . . 10
β’ ((π½ β π-Locally Comp
β§ π’ β π½ β§ π¦ β π’) β βπ β π« π’βπ€ β π½ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp)) |
10 | 5, 6, 8, 9 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β βπ β π« π’βπ€ β π½ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp)) |
11 | 3 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π½ βΎt π΄) β Top) |
12 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π½ β Top) |
13 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π΄ β (Clsdβπ½)) |
14 | | simprlr 779 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π€ β π½) |
15 | | elrestr 17318 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π΄ β (Clsdβπ½) β§ π€ β π½) β (π€ β© π΄) β (π½ βΎt π΄)) |
16 | 12, 13, 14, 15 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π€ β© π΄) β (π½ βΎt π΄)) |
17 | | simprr1 1222 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π¦ β π€) |
18 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π¦ β (π’ β© π΄)) |
19 | 18 | elin2d 4163 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π¦ β π΄) |
20 | 17, 19 | elind 4158 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π¦ β (π€ β© π΄)) |
21 | | opnneip 22493 |
. . . . . . . . . . . . . . 15
β’ (((π½ βΎt π΄) β Top β§ (π€ β© π΄) β (π½ βΎt π΄) β§ π¦ β (π€ β© π΄)) β (π€ β© π΄) β ((neiβ(π½ βΎt π΄))β{π¦})) |
22 | 11, 16, 20, 21 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π€ β© π΄) β ((neiβ(π½ βΎt π΄))β{π¦})) |
23 | | simprr2 1223 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π€ β π ) |
24 | 23 | ssrind 4199 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π€ β© π΄) β (π β© π΄)) |
25 | | inss2 4193 |
. . . . . . . . . . . . . . 15
β’ (π β© π΄) β π΄ |
26 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π½ =
βͺ π½ |
27 | 26 | cldss 22403 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β (Clsdβπ½) β π΄ β βͺ π½) |
28 | 13, 27 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π΄ β βͺ π½) |
29 | 26 | restuni 22536 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π΄ β βͺ π½)
β π΄ = βͺ (π½
βΎt π΄)) |
30 | 12, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π΄ = βͺ (π½ βΎt π΄)) |
31 | 25, 30 | sseqtrid 4000 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β βͺ
(π½ βΎt
π΄)) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ βͺ (π½
βΎt π΄) =
βͺ (π½ βΎt π΄) |
33 | 32 | ssnei2 22490 |
. . . . . . . . . . . . . 14
β’ ((((π½ βΎt π΄) β Top β§ (π€ β© π΄) β ((neiβ(π½ βΎt π΄))β{π¦})) β§ ((π€ β© π΄) β (π β© π΄) β§ (π β© π΄) β βͺ
(π½ βΎt
π΄))) β (π β© π΄) β ((neiβ(π½ βΎt π΄))β{π¦})) |
34 | 11, 22, 24, 31, 33 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β ((neiβ(π½ βΎt π΄))β{π¦})) |
35 | | simprll 778 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π β π« π’) |
36 | 35 | elpwid 4573 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π β π’) |
37 | 36 | ssrind 4199 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β (π’ β© π΄)) |
38 | | vex 3451 |
. . . . . . . . . . . . . . . 16
β’ π β V |
39 | 38 | inex1 5278 |
. . . . . . . . . . . . . . 15
β’ (π β© π΄) β V |
40 | 39 | elpw 4568 |
. . . . . . . . . . . . . 14
β’ ((π β© π΄) β π« (π’ β© π΄) β (π β© π΄) β (π’ β© π΄)) |
41 | 37, 40 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β π« (π’ β© π΄)) |
42 | 34, 41 | elind 4158 |
. . . . . . . . . . . 12
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))) |
43 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β π΄) |
44 | | restabs 22539 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ (π β© π΄) β π΄ β§ π΄ β (Clsdβπ½)) β ((π½ βΎt π΄) βΎt (π β© π΄)) = (π½ βΎt (π β© π΄))) |
45 | 12, 43, 13, 44 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π½ βΎt π΄) βΎt (π β© π΄)) = (π½ βΎt (π β© π΄))) |
46 | | inss1 4192 |
. . . . . . . . . . . . . . . 16
β’ (π β© π΄) β π |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β π ) |
48 | | restabs 22539 |
. . . . . . . . . . . . . . 15
β’ ((π½ β Top β§ (π β© π΄) β π β§ π β π« π’) β ((π½ βΎt π ) βΎt (π β© π΄)) = (π½ βΎt (π β© π΄))) |
49 | 12, 47, 35, 48 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π½ βΎt π ) βΎt (π β© π΄)) = (π½ βΎt (π β© π΄))) |
50 | 45, 49 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π½ βΎt π΄) βΎt (π β© π΄)) = ((π½ βΎt π ) βΎt (π β© π΄))) |
51 | | simprr3 1224 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π½ βΎt π ) β Comp) |
52 | | incom 4165 |
. . . . . . . . . . . . . . 15
β’ (π β© π΄) = (π΄ β© π ) |
53 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β© π ) = (π΄ β© π ) |
54 | | ineq1 4169 |
. . . . . . . . . . . . . . . . . 18
β’ (π£ = π΄ β (π£ β© π ) = (π΄ β© π )) |
55 | 54 | rspceeqv 3599 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β (Clsdβπ½) β§ (π΄ β© π ) = (π΄ β© π )) β βπ£ β (Clsdβπ½)(π΄ β© π ) = (π£ β© π )) |
56 | 13, 53, 55 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β βπ£ β (Clsdβπ½)(π΄ β© π ) = (π£ β© π )) |
57 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π’ β π½) |
58 | | elssuni 4902 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β π½ β π’ β βͺ π½) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π’ β βͺ π½) |
60 | 36, 59 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β π β βͺ π½) |
61 | 26 | restcld 22546 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π β βͺ π½)
β ((π΄ β© π ) β (Clsdβ(π½ βΎt π )) β βπ£ β (Clsdβπ½)(π΄ β© π ) = (π£ β© π ))) |
62 | 12, 60, 61 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π΄ β© π ) β (Clsdβ(π½ βΎt π )) β βπ£ β (Clsdβπ½)(π΄ β© π ) = (π£ β© π ))) |
63 | 56, 62 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π΄ β© π ) β (Clsdβ(π½ βΎt π ))) |
64 | 52, 63 | eqeltrid 2838 |
. . . . . . . . . . . . . 14
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β (π β© π΄) β (Clsdβ(π½ βΎt π ))) |
65 | | cmpcld 22776 |
. . . . . . . . . . . . . 14
β’ (((π½ βΎt π ) β Comp β§ (π β© π΄) β (Clsdβ(π½ βΎt π ))) β ((π½ βΎt π ) βΎt (π β© π΄)) β Comp) |
66 | 51, 64, 65 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π½ βΎt π ) βΎt (π β© π΄)) β Comp) |
67 | 50, 66 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β ((π½ βΎt π΄) βΎt (π β© π΄)) β Comp) |
68 | | oveq2 7369 |
. . . . . . . . . . . . . 14
β’ (π£ = (π β© π΄) β ((π½ βΎt π΄) βΎt π£) = ((π½ βΎt π΄) βΎt (π β© π΄))) |
69 | 68 | eleq1d 2819 |
. . . . . . . . . . . . 13
β’ (π£ = (π β© π΄) β (((π½ βΎt π΄) βΎt π£) β Comp β ((π½ βΎt π΄) βΎt (π β© π΄)) β Comp)) |
70 | 69 | rspcev 3583 |
. . . . . . . . . . . 12
β’ (((π β© π΄) β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄)) β§ ((π½ βΎt π΄) βΎt (π β© π΄)) β Comp) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp) |
71 | 42, 67, 70 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ ((π β π« π’ β§ π€ β π½) β§ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp))) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp) |
72 | 71 | expr 458 |
. . . . . . . . . 10
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β§ (π β π« π’ β§ π€ β π½)) β ((π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp)) |
73 | 72 | rexlimdvva 3202 |
. . . . . . . . 9
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β (βπ β π« π’βπ€ β π½ (π¦ β π€ β§ π€ β π β§ (π½ βΎt π ) β Comp) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp)) |
74 | 10, 73 | mpd 15 |
. . . . . . . 8
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§
(π’ β π½ β§ π¦ β (π’ β© π΄))) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp) |
75 | 74 | anassrs 469 |
. . . . . . 7
β’ ((((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§ π’ β π½) β§ π¦ β (π’ β© π΄)) β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp) |
76 | 75 | ralrimiva 3140 |
. . . . . 6
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§ π’ β π½) β βπ¦ β (π’ β© π΄)βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp) |
77 | | pweq 4578 |
. . . . . . . . 9
β’ (π₯ = (π’ β© π΄) β π« π₯ = π« (π’ β© π΄)) |
78 | 77 | ineq2d 4176 |
. . . . . . . 8
β’ (π₯ = (π’ β© π΄) β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯) = (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))) |
79 | 78 | rexeqdv 3313 |
. . . . . . 7
β’ (π₯ = (π’ β© π΄) β (βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp β βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp)) |
80 | 79 | raleqbi1dv 3306 |
. . . . . 6
β’ (π₯ = (π’ β© π΄) β (βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp β βπ¦ β (π’ β© π΄)βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« (π’ β© π΄))((π½ βΎt π΄) βΎt π£) β Comp)) |
81 | 76, 80 | syl5ibrcom 247 |
. . . . 5
β’ (((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β§ π’ β π½) β (π₯ = (π’ β© π΄) β βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp)) |
82 | 81 | rexlimdva 3149 |
. . . 4
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
(βπ’ β π½ π₯ = (π’ β© π΄) β βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp)) |
83 | 4, 82 | sylbid 239 |
. . 3
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
(π₯ β (π½ βΎt π΄) β βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp)) |
84 | 83 | ralrimiv 3139 |
. 2
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
βπ₯ β (π½ βΎt π΄)βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp) |
85 | | isnlly 22843 |
. 2
β’ ((π½ βΎt π΄) β π-Locally Comp
β ((π½
βΎt π΄)
β Top β§ βπ₯
β (π½
βΎt π΄)βπ¦ β π₯ βπ£ β (((neiβ(π½ βΎt π΄))β{π¦}) β© π« π₯)((π½ βΎt π΄) βΎt π£) β Comp)) |
86 | 3, 84, 85 | sylanbrc 584 |
1
β’ ((π½ β π-Locally Comp
β§ π΄ β
(Clsdβπ½)) β
(π½ βΎt
π΄) β π-Locally
Comp) |