Step | Hyp | Ref
| Expression |
1 | | llytop 22846 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
π β
Top) |
2 | | llyi 22848 |
. . . . . . 7
β’ ((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β βπ’ β π (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄)) |
3 | | simprr3 1224 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π βΎt π’) β π-Locally π΄) |
4 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π) |
5 | | ssidd 3971 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π’) |
6 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Locally π-Locally π΄) |
7 | 6, 1 | syl 17 |
. . . . . . . . . . 11
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Top) |
8 | | restopn2 22551 |
. . . . . . . . . . 11
β’ ((π β Top β§ π’ β π) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
9 | 7, 4, 8 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
10 | 4, 5, 9 | mpbir2and 712 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β (π βΎt π’)) |
11 | | simprr2 1223 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π¦ β π’) |
12 | | nlly2i 22850 |
. . . . . . . . 9
β’ (((π βΎt π’) β π-Locally π΄ β§ π’ β (π βΎt π’) β§ π¦ β π’) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
13 | 3, 10, 11, 12 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
14 | | restopn2 22551 |
. . . . . . . . . . . . . 14
β’ ((π β Top β§ π’ β π) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
15 | 7, 4, 14 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
16 | 15 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
17 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π β Top) |
18 | | simpr2l 1233 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π) |
19 | | simpr31 1264 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π¦ β π§) |
20 | | opnneip 22493 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Top β§ π§ β π β§ π¦ β π§) β π§ β ((neiβπ)β{π¦})) |
21 | 17, 18, 19, 20 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β ((neiβπ)β{π¦})) |
22 | | simpr32 1265 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π£) |
23 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π’) |
24 | 23 | elpwid 4573 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π’) |
25 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π) |
26 | | elssuni 4902 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β π β π’ β βͺ π) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β βͺ π) |
28 | 24, 27 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β βͺ π) |
29 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π =
βͺ π |
30 | 29 | ssnei2 22490 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Top β§ π§ β ((neiβπ)β{π¦})) β§ (π§ β π£ β§ π£ β βͺ π)) β π£ β ((neiβπ)β{π¦})) |
31 | 17, 21, 22, 28, 30 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β ((neiβπ)β{π¦})) |
32 | | simprr1 1222 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π₯) |
33 | 32 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π₯) |
34 | 24, 33 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π₯) |
35 | | velpw 4569 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β π« π₯ β π£ β π₯) |
36 | 34, 35 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π₯) |
37 | 31, 36 | elind 4158 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β (((neiβπ)β{π¦}) β© π« π₯)) |
38 | | restabs 22539 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Top β§ π£ β π’ β§ π’ β π) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
39 | 17, 24, 25, 38 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
40 | | simpr33 1266 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) β π΄) |
41 | 39, 40 | eqeltrrd 2835 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π βΎt π£) β π΄) |
42 | 37, 41 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄)) |
43 | 42 | 3exp2 1355 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π£ β π« π’ β ((π§ β π β§ π§ β π’) β ((π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))))) |
44 | 43 | imp 408 |
. . . . . . . . . . . 12
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β ((π§ β π β§ π§ β π’) β ((π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄)))) |
45 | 16, 44 | sylbid 239 |
. . . . . . . . . . 11
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (π§ β (π βΎt π’) β ((π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄)))) |
46 | 45 | rexlimdv 3147 |
. . . . . . . . . 10
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))) |
47 | 46 | expimpd 455 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β ((π£ β π« π’ β§ βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))) |
48 | 47 | reximdv2 3158 |
. . . . . . . 8
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄)) |
49 | 13, 48 | mpd 15 |
. . . . . . 7
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
50 | 2, 49 | rexlimddv 3155 |
. . . . . 6
β’ ((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
51 | 50 | 3expb 1121 |
. . . . 5
β’ ((π β Locally
π-Locally π΄ β§
(π₯ β π β§ π¦ β π₯)) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
52 | 51 | ralrimivva 3194 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
53 | | isnlly 22843 |
. . . 4
β’ (π β π-Locally π΄ β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄)) |
54 | 1, 52, 53 | sylanbrc 584 |
. . 3
β’ (π β Locally
π-Locally π΄ β
π β π-Locally
π΄) |
55 | 54 | ssriv 3952 |
. 2
β’ Locally
π-Locally π΄ β
π-Locally π΄ |
56 | | nllyrest 22860 |
. . . . 5
β’ ((π β π-Locally π΄ β§ π₯ β π) β (π βΎt π₯) β π-Locally π΄) |
57 | 56 | adantl 483 |
. . . 4
β’
((β€ β§ (π
β π-Locally π΄
β§ π₯ β π)) β (π βΎt π₯) β π-Locally π΄) |
58 | | nllytop 22847 |
. . . . . 6
β’ (π β π-Locally π΄ β π β Top) |
59 | 58 | ssriv 3952 |
. . . . 5
β’
π-Locally π΄
β Top |
60 | 59 | a1i 11 |
. . . 4
β’ (β€
β π-Locally π΄
β Top) |
61 | 57, 60 | restlly 22857 |
. . 3
β’ (β€
β π-Locally π΄
β Locally π-Locally π΄) |
62 | 61 | mptru 1549 |
. 2
β’
π-Locally π΄
β Locally π-Locally π΄ |
63 | 55, 62 | eqssi 3964 |
1
β’ Locally
π-Locally π΄ =
π-Locally π΄ |