Step | Hyp | Ref
| Expression |
1 | | nllytop 21276 |
. . . . . 6
𝑛Locally
|
2 | 1 | adantl 482 |
. . . . 5
𝑛Locally
|
3 | | nlly2i 21279 |
. . . . . . . . 9
𝑛Locally
↾t |
4 | 3 | 3adant1l 1318 |
. . . . . . . 8
𝑛Locally
↾t |
5 | | simprl 794 |
. . . . . . . . . . . . 13
𝑛Locally
↾t |
6 | | simprr2 1110 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t |
7 | | simplr 792 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t |
8 | 7 | elpwid 4170 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t |
9 | 6, 8 | sstrd 3613 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t |
10 | | selpw 4165 |
. . . . . . . . . . . . . 14
|
11 | 9, 10 | sylibr 224 |
. . . . . . . . . . . . 13
𝑛Locally
↾t |
12 | 5, 11 | elind 3798 |
. . . . . . . . . . . 12
𝑛Locally
↾t |
13 | | simprr1 1109 |
. . . . . . . . . . . 12
𝑛Locally
↾t |
14 | | simpll1 1100 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t
𝑛Locally |
15 | 14 | simprd 479 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t 𝑛Locally |
16 | 15, 1 | syl 17 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t |
17 | | restabs 20969 |
. . . . . . . . . . . . . 14
↾t ↾t ↾t |
18 | 16, 6, 7, 17 | syl3anc 1326 |
. . . . . . . . . . . . 13
𝑛Locally
↾t ↾t ↾t ↾t |
19 | | simprr3 1111 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t ↾t |
20 | 14 | simpld 475 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t |
21 | | restlly.1 |
. . . . . . . . . . . . . . . . 17
↾t |
22 | 21 | expr 643 |
. . . . . . . . . . . . . . . 16
↾t |
23 | 22 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
↾t |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t
↾t |
25 | | df-ss 3588 |
. . . . . . . . . . . . . . . 16
|
26 | 6, 25 | sylib 208 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t |
27 | | elrestr 16089 |
. . . . . . . . . . . . . . . 16
↾t |
28 | 16, 7, 5, 27 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t ↾t |
29 | 26, 28 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t ↾t |
30 | | eleq2 2690 |
. . . . . . . . . . . . . . . 16
↾t
↾t |
31 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
↾t ↾t ↾t ↾t |
32 | 31 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
↾t ↾t
↾t
↾t |
33 | 30, 32 | imbi12d 334 |
. . . . . . . . . . . . . . 15
↾t ↾t
↾t ↾t ↾t |
34 | 33 | rspcv 3305 |
. . . . . . . . . . . . . 14
↾t
↾t
↾t ↾t ↾t |
35 | 19, 24, 29, 34 | syl3c 66 |
. . . . . . . . . . . . 13
𝑛Locally
↾t ↾t ↾t |
36 | 18, 35 | eqeltrrd 2702 |
. . . . . . . . . . . 12
𝑛Locally
↾t ↾t |
37 | 12, 13, 36 | jca32 558 |
. . . . . . . . . . 11
𝑛Locally
↾t
↾t |
38 | 37 | ex 450 |
. . . . . . . . . 10
𝑛Locally
↾t
↾t |
39 | 38 | reximdv2 3014 |
. . . . . . . . 9
𝑛Locally
↾t ↾t |
40 | 39 | rexlimdva 3031 |
. . . . . . . 8
𝑛Locally
↾t ↾t |
41 | 4, 40 | mpd 15 |
. . . . . . 7
𝑛Locally
↾t |
42 | 41 | 3expb 1266 |
. . . . . 6
𝑛Locally
↾t |
43 | 42 | ralrimivva 2971 |
. . . . 5
𝑛Locally
↾t |
44 | | islly 21271 |
. . . . 5
Locally
↾t |
45 | 2, 43, 44 | sylanbrc 698 |
. . . 4
𝑛Locally
Locally |
46 | 45 | ex 450 |
. . 3
𝑛Locally
Locally |
47 | 46 | ssrdv 3609 |
. 2
𝑛Locally Locally |
48 | | llyssnlly 21281 |
. . 3
Locally 𝑛Locally |
49 | 48 | a1i 11 |
. 2
Locally
𝑛Locally |
50 | 47, 49 | eqssd 3620 |
1
𝑛Locally Locally |