Step | Hyp | Ref
| Expression |
1 | | resttop 20964 |
. . 3
↾t |
2 | | islly 21271 |
. . . 4
↾t Locally
↾t ↾t
↾t ↾t ↾t |
3 | 2 | baib 944 |
. . 3
↾t ↾t Locally
↾t
↾t ↾t ↾t |
4 | 1, 3 | syl 17 |
. 2
↾t Locally
↾t
↾t ↾t ↾t |
5 | | vex 3203 |
. . . . 5
|
6 | 5 | inex1 4799 |
. . . 4
|
7 | 6 | a1i 11 |
. . 3
|
8 | | elrest 16088 |
. . 3
↾t
|
9 | | simpr 477 |
. . . . 5
|
10 | 9 | raleqdv 3144 |
. . . 4
↾t
↾t
↾t
↾t
↾t
↾t |
11 | | elin 3796 |
. . . . . . . . 9
↾t
↾t |
12 | 11 | anbi1i 731 |
. . . . . . . 8
↾t ↾t ↾t ↾t ↾t ↾t |
13 | | anass 681 |
. . . . . . . 8
↾t ↾t ↾t
↾t ↾t ↾t |
14 | 12, 13 | bitri 264 |
. . . . . . 7
↾t ↾t ↾t
↾t ↾t ↾t |
15 | 14 | rexbii2 3039 |
. . . . . 6
↾t
↾t
↾t ↾t ↾t ↾t |
16 | | vex 3203 |
. . . . . . . . 9
|
17 | 16 | inex1 4799 |
. . . . . . . 8
|
18 | 17 | a1i 11 |
. . . . . . 7
|
19 | | elrest 16088 |
. . . . . . . 8
↾t
|
20 | 19 | ad2antrr 762 |
. . . . . . 7
↾t
|
21 | | 3anass 1042 |
. . . . . . . 8
↾t ↾t ↾t
↾t |
22 | | simpr 477 |
. . . . . . . . . . 11
|
23 | | simpllr 799 |
. . . . . . . . . . 11
|
24 | 22, 23 | sseq12d 3634 |
. . . . . . . . . 10
|
25 | | selpw 4165 |
. . . . . . . . . 10
|
26 | | inss2 3834 |
. . . . . . . . . . . 12
|
27 | 26 | biantru 526 |
. . . . . . . . . . 11
|
28 | | ssin 3835 |
. . . . . . . . . . 11
|
29 | 27, 28 | bitri 264 |
. . . . . . . . . 10
|
30 | 24, 25, 29 | 3bitr4g 303 |
. . . . . . . . 9
|
31 | 22 | eleq2d 2687 |
. . . . . . . . . 10
|
32 | | inss2 3834 |
. . . . . . . . . . . . 13
|
33 | | simplr 792 |
. . . . . . . . . . . . 13
|
34 | 32, 33 | sseldi 3601 |
. . . . . . . . . . . 12
|
35 | 34 | biantrud 528 |
. . . . . . . . . . 11
|
36 | | elin 3796 |
. . . . . . . . . . 11
|
37 | 35, 36 | syl6bbr 278 |
. . . . . . . . . 10
|
38 | 31, 37 | bitr4d 271 |
. . . . . . . . 9
|
39 | 22 | oveq2d 6666 |
. . . . . . . . . . 11
↾t ↾t ↾t
↾t |
40 | | simp-4l 806 |
. . . . . . . . . . . 12
|
41 | 26 | a1i 11 |
. . . . . . . . . . . 12
|
42 | | simplr 792 |
. . . . . . . . . . . . 13
|
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . 12
|
44 | | restabs 20969 |
. . . . . . . . . . . 12
↾t
↾t
↾t |
45 | 40, 41, 43, 44 | syl3anc 1326 |
. . . . . . . . . . 11
↾t ↾t ↾t |
46 | 39, 45 | eqtrd 2656 |
. . . . . . . . . 10
↾t ↾t ↾t |
47 | 46 | eleq1d 2686 |
. . . . . . . . 9
↾t ↾t ↾t |
48 | 30, 38, 47 | 3anbi123d 1399 |
. . . . . . . 8
↾t
↾t
↾t |
49 | 21, 48 | syl5bbr 274 |
. . . . . . 7
↾t ↾t
↾t |
50 | 18, 20, 49 | rexxfr2d 4883 |
. . . . . 6
↾t ↾t ↾t
↾t |
51 | 15, 50 | syl5bb 272 |
. . . . 5
↾t ↾t ↾t
↾t |
52 | 51 | ralbidva 2985 |
. . . 4
↾t ↾t ↾t
↾t |
53 | 10, 52 | bitrd 268 |
. . 3
↾t
↾t
↾t
↾t |
54 | 7, 8, 53 | ralxfr2d 4882 |
. 2
↾t
↾t ↾t ↾t
↾t |
55 | 4, 54 | bitrd 268 |
1
↾t Locally
↾t |