Step | Hyp | Ref
| Expression |
1 | | llytop 23327 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
π β
Top) |
2 | | llyi 23329 |
. . . . . . 7
β’ ((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β βπ’ β π (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄)) |
3 | | simprr3 1220 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π βΎt π’) β π-Locally π΄) |
4 | | simprl 768 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π) |
5 | | ssidd 4000 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π’) |
6 | | simpl1 1188 |
. . . . . . . . . . . 12
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Locally π-Locally π΄) |
7 | 6, 1 | syl 17 |
. . . . . . . . . . 11
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Top) |
8 | | restopn2 23032 |
. . . . . . . . . . 11
β’ ((π β Top β§ π’ β π) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
9 | 7, 4, 8 | syl2anc 583 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
10 | 4, 5, 9 | mpbir2and 710 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β (π βΎt π’)) |
11 | | simprr2 1219 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π¦ β π’) |
12 | | nlly2i 23331 |
. . . . . . . . 9
β’ (((π βΎt π’) β π-Locally π΄ β§ π’ β (π βΎt π’) β§ π¦ β π’) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
13 | 3, 10, 11, 12 | syl3anc 1368 |
. . . . . . . 8
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
14 | | restopn2 23032 |
. . . . . . . . . . . . . 14
β’ ((π β Top β§ π’ β π) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
15 | 7, 4, 14 | syl2anc 583 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
17 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π β Top) |
18 | | simpr2l 1229 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π) |
19 | | simpr31 1260 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π¦ β π§) |
20 | | opnneip 22974 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Top β§ π§ β π β§ π¦ β π§) β π§ β ((neiβπ)β{π¦})) |
21 | 17, 18, 19, 20 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β ((neiβπ)β{π¦})) |
22 | | simpr32 1261 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π£) |
23 | | simpr1 1191 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π’) |
24 | 23 | elpwid 4606 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π’) |
25 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π) |
26 | | elssuni 4934 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β π β π’ β βͺ π) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β βͺ π) |
28 | 24, 27 | sstrd 3987 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β βͺ π) |
29 | | eqid 2726 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π =
βͺ π |
30 | 29 | ssnei2 22971 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Top β§ π§ β ((neiβπ)β{π¦})) β§ (π§ β π£ β§ π£ β βͺ π)) β π£ β ((neiβπ)β{π¦})) |
31 | 17, 21, 22, 28, 30 | syl22anc 836 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β ((neiβπ)β{π¦})) |
32 | | simprr1 1218 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π₯) |
33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π₯) |
34 | 24, 33 | sstrd 3987 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π₯) |
35 | | velpw 4602 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β π« π₯ β π£ β π₯) |
36 | 34, 35 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π₯) |
37 | 31, 36 | elind 4189 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β (((neiβπ)β{π¦}) β© π« π₯)) |
38 | | restabs 23020 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Top β§ π£ β π’ β§ π’ β π) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
39 | 17, 24, 25, 38 | syl3anc 1368 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
40 | | simpr33 1262 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) β π΄) |
41 | 39, 40 | eqeltrrd 2828 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π βΎt π£) β π΄) |
42 | 37, 41 | jca 511 |
. . . . . . . . . . . . . 14
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄)) |
43 | 42 | 3exp2 1351 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π£ β π« π’ β ((π§ β π β§ π§ β π’) β ((π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))))) |
44 | 43 | imp 406 |
. . . . . . . . . . . 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 453 |
. . . . . . . . 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 1117 |
. . . . 5
β’ ((π β Locally
π-Locally π΄ β§
(π₯ β π β§ π¦ β π₯)) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
52 | 51 | ralrimivva 3194 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
53 | | isnlly 23324 |
. . . 4
β’ (π β π-Locally π΄ β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄)) |
54 | 1, 52, 53 | sylanbrc 582 |
. . 3
β’ (π β Locally
π-Locally π΄ β
π β π-Locally
π΄) |
55 | 54 | ssriv 3981 |
. 2
β’ Locally
π-Locally π΄ β
π-Locally π΄ |
56 | | nllyrest 23341 |
. . . . 5
β’ ((π β π-Locally π΄ β§ π₯ β π) β (π βΎt π₯) β π-Locally π΄) |
57 | 56 | adantl 481 |
. . . 4
β’
((β€ β§ (π
β π-Locally π΄
β§ π₯ β π)) β (π βΎt π₯) β π-Locally π΄) |
58 | | nllytop 23328 |
. . . . . 6
β’ (π β π-Locally π΄ β π β Top) |
59 | 58 | ssriv 3981 |
. . . . 5
β’
π-Locally π΄
β Top |
60 | 59 | a1i 11 |
. . . 4
β’ (β€
β π-Locally π΄
β Top) |
61 | 57, 60 | restlly 23338 |
. . 3
β’ (β€
β π-Locally π΄
β Locally π-Locally π΄) |
62 | 61 | mptru 1540 |
. 2
β’
π-Locally π΄
β Locally π-Locally π΄ |
63 | 55, 62 | eqssi 3993 |
1
β’ Locally
π-Locally π΄ =
π-Locally π΄ |