Step | Hyp | Ref
| Expression |
1 | | nllytop 21276 |
. . 3
𝑛Locally
|
2 | | resttop 20964 |
. . 3
↾t |
3 | 1, 2 | sylan 488 |
. 2
𝑛Locally ↾t |
4 | | restopn2 20981 |
. . . . 5
↾t
|
5 | 1, 4 | sylan 488 |
. . . 4
𝑛Locally ↾t |
6 | | simp1l 1085 |
. . . . . . . . 9
𝑛Locally
𝑛Locally |
7 | | simp2l 1087 |
. . . . . . . . 9
𝑛Locally
|
8 | | simp3 1063 |
. . . . . . . . 9
𝑛Locally
|
9 | | nlly2i 21279 |
. . . . . . . . 9
𝑛Locally
↾t |
10 | 6, 7, 8, 9 | syl3anc 1326 |
. . . . . . . 8
𝑛Locally
↾t |
11 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t |
12 | 11 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t ↾t |
13 | | simp3l 1089 |
. . . . . . . . . . . . . . . . 17
𝑛Locally
↾t |
14 | | simp3r2 1170 |
. . . . . . . . . . . . . . . . . 18
𝑛Locally
↾t |
15 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . 20
𝑛Locally
↾t |
16 | 15 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . 19
𝑛Locally
↾t |
17 | | simp12r 1175 |
. . . . . . . . . . . . . . . . . . 19
𝑛Locally
↾t |
18 | 16, 17 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
𝑛Locally
↾t |
19 | 14, 18 | sstrd 3613 |
. . . . . . . . . . . . . . . . 17
𝑛Locally
↾t |
20 | 6 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
𝑛Locally
↾t 𝑛Locally |
21 | 20, 1 | syl 17 |
. . . . . . . . . . . . . . . . . 18
𝑛Locally
↾t |
22 | | simp11r 1173 |
. . . . . . . . . . . . . . . . . 18
𝑛Locally
↾t |
23 | | restopn2 20981 |
. . . . . . . . . . . . . . . . . 18
↾t
|
24 | 21, 22, 23 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
𝑛Locally
↾t
↾t
|
25 | 13, 19, 24 | mpbir2and 957 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t ↾t |
26 | | simp3r1 1169 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t |
27 | | opnneip 20923 |
. . . . . . . . . . . . . . . 16
↾t ↾t ↾t |
28 | 12, 25, 26, 27 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t ↾t |
29 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . 18
|
30 | 22, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
𝑛Locally
↾t |
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
32 | 31 | restuni 20966 |
. . . . . . . . . . . . . . . . 17
↾t |
33 | 21, 30, 32 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
𝑛Locally
↾t
↾t |
34 | 18, 33 | sseqtrd 3641 |
. . . . . . . . . . . . . . 15
𝑛Locally
↾t ↾t |
35 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
↾t
↾t |
36 | 35 | ssnei2 20920 |
. . . . . . . . . . . . . . 15
↾t ↾t ↾t ↾t |
37 | 12, 28, 14, 34, 36 | syl22anc 1327 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t ↾t |
38 | 37, 15 | elind 3798 |
. . . . . . . . . . . . 13
𝑛Locally
↾t ↾t |
39 | | restabs 20969 |
. . . . . . . . . . . . . . 15
↾t
↾t
↾t |
40 | 21, 18, 22, 39 | syl3anc 1326 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t ↾t ↾t ↾t |
41 | | simp3r3 1171 |
. . . . . . . . . . . . . 14
𝑛Locally
↾t ↾t |
42 | 40, 41 | eqeltrd 2701 |
. . . . . . . . . . . . 13
𝑛Locally
↾t ↾t ↾t |
43 | 38, 42 | jca 554 |
. . . . . . . . . . . 12
𝑛Locally
↾t
↾t ↾t ↾t |
44 | 43 | 3expa 1265 |
. . . . . . . . . . 11
𝑛Locally
↾t
↾t ↾t ↾t |
45 | 44 | rexlimdvaa 3032 |
. . . . . . . . . 10
𝑛Locally
↾t ↾t ↾t ↾t |
46 | 45 | expimpd 629 |
. . . . . . . . 9
𝑛Locally
↾t ↾t ↾t ↾t |
47 | 46 | reximdv2 3014 |
. . . . . . . 8
𝑛Locally
↾t
↾t ↾t ↾t |
48 | 10, 47 | mpd 15 |
. . . . . . 7
𝑛Locally
↾t ↾t ↾t |
49 | 48 | 3expa 1265 |
. . . . . 6
𝑛Locally
↾t ↾t ↾t |
50 | 49 | ralrimiva 2966 |
. . . . 5
𝑛Locally
↾t ↾t ↾t |
51 | 50 | ex 450 |
. . . 4
𝑛Locally
↾t ↾t ↾t |
52 | 5, 51 | sylbid 230 |
. . 3
𝑛Locally ↾t
↾t ↾t ↾t |
53 | 52 | ralrimiv 2965 |
. 2
𝑛Locally
↾t
↾t ↾t ↾t |
54 | | isnlly 21272 |
. 2
↾t 𝑛Locally
↾t ↾t
↾t ↾t ↾t |
55 | 3, 53, 54 | sylanbrc 698 |
1
𝑛Locally ↾t 𝑛Locally |