Step | Hyp | Ref
| Expression |
1 | | llytop 22975 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
π β
Top) |
2 | | llyi 22977 |
. . . . . . 7
β’ ((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β βπ’ β π (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄)) |
3 | | simprr3 1223 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π βΎt π’) β π-Locally π΄) |
4 | | simprl 769 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π) |
5 | | ssidd 4005 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π’) |
6 | | simpl1 1191 |
. . . . . . . . . . . 12
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Locally π-Locally π΄) |
7 | 6, 1 | syl 17 |
. . . . . . . . . . 11
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π β Top) |
8 | | restopn2 22680 |
. . . . . . . . . . 11
β’ ((π β Top β§ π’ β π) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
9 | 7, 4, 8 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π’ β (π βΎt π’) β (π’ β π β§ π’ β π’))) |
10 | 4, 5, 9 | mpbir2and 711 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β (π βΎt π’)) |
11 | | simprr2 1222 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π¦ β π’) |
12 | | nlly2i 22979 |
. . . . . . . . 9
β’ (((π βΎt π’) β π-Locally π΄ β§ π’ β (π βΎt π’) β§ π¦ β π’) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
13 | 3, 10, 11, 12 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β βπ£ β π« π’βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) |
14 | | restopn2 22680 |
. . . . . . . . . . . . . 14
β’ ((π β Top β§ π’ β π) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
15 | 7, 4, 14 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
16 | 15 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (π§ β (π βΎt π’) β (π§ β π β§ π§ β π’))) |
17 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π β Top) |
18 | | simpr2l 1232 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π) |
19 | | simpr31 1263 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π¦ β π§) |
20 | | opnneip 22622 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Top β§ π§ β π β§ π¦ β π§) β π§ β ((neiβπ)β{π¦})) |
21 | 17, 18, 19, 20 | syl3anc 1371 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β ((neiβπ)β{π¦})) |
22 | | simpr32 1264 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π§ β π£) |
23 | | simpr1 1194 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π’) |
24 | 23 | elpwid 4611 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π’) |
25 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π) |
26 | | elssuni 4941 |
. . . . . . . . . . . . . . . . . . 19
β’ (π’ β π β π’ β βͺ π) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β βͺ π) |
28 | 24, 27 | sstrd 3992 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β βͺ π) |
29 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π =
βͺ π |
30 | 29 | ssnei2 22619 |
. . . . . . . . . . . . . . . . 17
β’ (((π β Top β§ π§ β ((neiβπ)β{π¦})) β§ (π§ β π£ β§ π£ β βͺ π)) β π£ β ((neiβπ)β{π¦})) |
31 | 17, 21, 22, 28, 30 | syl22anc 837 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β ((neiβπ)β{π¦})) |
32 | | simprr1 1221 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β π’ β π₯) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π’ β π₯) |
34 | 24, 33 | sstrd 3992 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π₯) |
35 | | velpw 4607 |
. . . . . . . . . . . . . . . . 17
β’ (π£ β π« π₯ β π£ β π₯) |
36 | 34, 35 | sylibr 233 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β π« π₯) |
37 | 31, 36 | elind 4194 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β π£ β (((neiβπ)β{π¦}) β© π« π₯)) |
38 | | restabs 22668 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Top β§ π£ β π’ β§ π’ β π) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
39 | 17, 24, 25, 38 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) = (π βΎt π£)) |
40 | | simpr33 1265 |
. . . . . . . . . . . . . . . 16
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β ((π βΎt π’) βΎt π£) β π΄) |
41 | 39, 40 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π βΎt π£) β π΄) |
42 | 37, 41 | jca 512 |
. . . . . . . . . . . . . 14
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ (π£ β π« π’ β§ (π§ β π β§ π§ β π’) β§ (π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄))) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄)) |
43 | 42 | 3exp2 1354 |
. . . . . . . . . . . . 13
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β (π£ β π« π’ β ((π§ β π β§ π§ β π’) β ((π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))))) |
44 | 43 | imp 407 |
. . . . . . . . . . . 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 3153 |
. . . . . . . . . 10
β’ ((((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β§ π£ β π« π’) β (βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))) |
47 | 46 | expimpd 454 |
. . . . . . . . 9
β’ (((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β§ (π’ β π β§ (π’ β π₯ β§ π¦ β π’ β§ (π βΎt π’) β π-Locally π΄))) β ((π£ β π« π’ β§ βπ§ β (π βΎt π’)(π¦ β π§ β§ π§ β π£ β§ ((π βΎt π’) βΎt π£) β π΄)) β (π£ β (((neiβπ)β{π¦}) β© π« π₯) β§ (π βΎt π£) β π΄))) |
48 | 47 | reximdv2 3164 |
. . . . . . . 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 3161 |
. . . . . 6
β’ ((π β Locally
π-Locally π΄ β§
π₯ β π β§ π¦ β π₯) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
51 | 50 | 3expb 1120 |
. . . . 5
β’ ((π β Locally
π-Locally π΄ β§
(π₯ β π β§ π¦ β π₯)) β βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
52 | 51 | ralrimivva 3200 |
. . . 4
β’ (π β Locally
π-Locally π΄ β
βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄) |
53 | | isnlly 22972 |
. . . 4
β’ (π β π-Locally π΄ β (π β Top β§ βπ₯ β π βπ¦ β π₯ βπ£ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π£) β π΄)) |
54 | 1, 52, 53 | sylanbrc 583 |
. . 3
β’ (π β Locally
π-Locally π΄ β
π β π-Locally
π΄) |
55 | 54 | ssriv 3986 |
. 2
β’ Locally
π-Locally π΄ β
π-Locally π΄ |
56 | | nllyrest 22989 |
. . . . 5
β’ ((π β π-Locally π΄ β§ π₯ β π) β (π βΎt π₯) β π-Locally π΄) |
57 | 56 | adantl 482 |
. . . 4
β’
((β€ β§ (π
β π-Locally π΄
β§ π₯ β π)) β (π βΎt π₯) β π-Locally π΄) |
58 | | nllytop 22976 |
. . . . . 6
β’ (π β π-Locally π΄ β π β Top) |
59 | 58 | ssriv 3986 |
. . . . 5
β’
π-Locally π΄
β Top |
60 | 59 | a1i 11 |
. . . 4
β’ (β€
β π-Locally π΄
β Top) |
61 | 57, 60 | restlly 22986 |
. . 3
β’ (β€
β π-Locally π΄
β Locally π-Locally π΄) |
62 | 61 | mptru 1548 |
. 2
β’
π-Locally π΄
β Locally π-Locally π΄ |
63 | 55, 62 | eqssi 3998 |
1
β’ Locally
π-Locally π΄ =
π-Locally π΄ |