Step | Hyp | Ref
| Expression |
1 | | llytop 21275 |
. . . 4
Locally 𝑛Locally |
2 | | llyi 21277 |
. . . . . . 7
Locally
𝑛Locally
↾t
𝑛Locally |
3 | | simprr3 1111 |
. . . . . . . . 9
Locally 𝑛Locally
↾t 𝑛Locally ↾t 𝑛Locally |
4 | | simprl 794 |
. . . . . . . . . 10
Locally 𝑛Locally
↾t 𝑛Locally |
5 | | ssid 3624 |
. . . . . . . . . . 11
|
6 | 5 | a1i 11 |
. . . . . . . . . 10
Locally 𝑛Locally
↾t 𝑛Locally |
7 | | simpl1 1064 |
. . . . . . . . . . . 12
Locally 𝑛Locally
↾t 𝑛Locally Locally 𝑛Locally |
8 | 7, 1 | syl 17 |
. . . . . . . . . . 11
Locally 𝑛Locally
↾t 𝑛Locally |
9 | | restopn2 20981 |
. . . . . . . . . . 11
↾t
|
10 | 8, 4, 9 | syl2anc 693 |
. . . . . . . . . 10
Locally 𝑛Locally
↾t 𝑛Locally ↾t |
11 | 4, 6, 10 | mpbir2and 957 |
. . . . . . . . 9
Locally 𝑛Locally
↾t 𝑛Locally
↾t |
12 | | simprr2 1110 |
. . . . . . . . 9
Locally 𝑛Locally
↾t 𝑛Locally |
13 | | nlly2i 21279 |
. . . . . . . . 9
↾t 𝑛Locally
↾t
↾t ↾t
↾t |
14 | 3, 11, 12, 13 | syl3anc 1326 |
. . . . . . . 8
Locally 𝑛Locally
↾t 𝑛Locally
↾t ↾t
↾t |
15 | | restopn2 20981 |
. . . . . . . . . . . . . 14
↾t
|
16 | 8, 4, 15 | syl2anc 693 |
. . . . . . . . . . . . 13
Locally 𝑛Locally
↾t 𝑛Locally ↾t |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
Locally 𝑛Locally
↾t 𝑛Locally ↾t
|
18 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
19 | | simpr2l 1120 |
. . . . . . . . . . . . . . . . . 18
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
20 | | simpr31 1151 |
. . . . . . . . . . . . . . . . . 18
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
21 | | opnneip 20923 |
. . . . . . . . . . . . . . . . . 18
|
22 | 18, 19, 20, 21 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
23 | | simpr32 1152 |
. . . . . . . . . . . . . . . . 17
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
24 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . 19
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
25 | 24 | elpwid 4170 |
. . . . . . . . . . . . . . . . . 18
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
26 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
27 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
29 | 25, 28 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30 | ssnei2 20920 |
. . . . . . . . . . . . . . . . 17
|
32 | 18, 22, 23, 29, 31 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
33 | | simprr1 1109 |
. . . . . . . . . . . . . . . . . . 19
Locally 𝑛Locally
↾t 𝑛Locally |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
35 | 25, 34 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
36 | | selpw 4165 |
. . . . . . . . . . . . . . . . 17
|
37 | 35, 36 | sylibr 224 |
. . . . . . . . . . . . . . . 16
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
38 | 32, 37 | elind 3798 |
. . . . . . . . . . . . . . 15
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t |
39 | | restabs 20969 |
. . . . . . . . . . . . . . . . 17
↾t
↾t
↾t |
40 | 18, 25, 26, 39 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t ↾t ↾t ↾t |
41 | | simpr33 1153 |
. . . . . . . . . . . . . . . 16
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t ↾t ↾t |
42 | 40, 41 | eqeltrrd 2702 |
. . . . . . . . . . . . . . 15
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t ↾t |
43 | 38, 42 | jca 554 |
. . . . . . . . . . . . . 14
Locally 𝑛Locally
↾t 𝑛Locally
↾t
↾t
↾t |
44 | 43 | 3exp2 1285 |
. . . . . . . . . . . . 13
Locally 𝑛Locally
↾t 𝑛Locally ↾t ↾t
↾t |
45 | 44 | imp 445 |
. . . . . . . . . . . 12
Locally 𝑛Locally
↾t 𝑛Locally ↾t ↾t
↾t |
46 | 17, 45 | sylbid 230 |
. . . . . . . . . . 11
Locally 𝑛Locally
↾t 𝑛Locally ↾t ↾t ↾t
↾t |
47 | 46 | rexlimdv 3030 |
. . . . . . . . . 10
Locally 𝑛Locally
↾t 𝑛Locally
↾t ↾t
↾t ↾t |
48 | 47 | expimpd 629 |
. . . . . . . . 9
Locally 𝑛Locally
↾t 𝑛Locally
↾t ↾t
↾t ↾t |
49 | 48 | reximdv2 3014 |
. . . . . . . 8
Locally 𝑛Locally
↾t 𝑛Locally
↾t ↾t
↾t ↾t |
50 | 14, 49 | mpd 15 |
. . . . . . 7
Locally 𝑛Locally
↾t 𝑛Locally ↾t |
51 | 2, 50 | rexlimddv 3035 |
. . . . . 6
Locally
𝑛Locally
↾t |
52 | 51 | 3expb 1266 |
. . . . 5
Locally
𝑛Locally
↾t |
53 | 52 | ralrimivva 2971 |
. . . 4
Locally 𝑛Locally
↾t |
54 | | isnlly 21272 |
. . . 4
𝑛Locally
↾t |
55 | 1, 53, 54 | sylanbrc 698 |
. . 3
Locally 𝑛Locally 𝑛Locally |
56 | 55 | ssriv 3607 |
. 2
Locally
𝑛Locally 𝑛Locally
|
57 | | nllyrest 21289 |
. . . . 5
𝑛Locally ↾t 𝑛Locally |
58 | 57 | adantl 482 |
. . . 4
𝑛Locally
↾t 𝑛Locally |
59 | | nllytop 21276 |
. . . . . 6
𝑛Locally
|
60 | 59 | ssriv 3607 |
. . . . 5
𝑛Locally
|
61 | 60 | a1i 11 |
. . . 4
𝑛Locally |
62 | 58, 61 | restlly 21286 |
. . 3
𝑛Locally Locally 𝑛Locally |
63 | 62 | trud 1493 |
. 2
𝑛Locally
Locally
𝑛Locally |
64 | 56, 63 | eqssi 3619 |
1
Locally
𝑛Locally 𝑛Locally |