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 | 1 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
Locally
Locally
|
8 | 7 | adantr 481 |
. . . . . . . . . . 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 | | llyi 21277 |
. . . . . . . . 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 |
. . . . . . . . . . . 12
↾t
|
16 | 8, 4, 15 | syl2anc 693 |
. . . . . . . . . . 11
Locally Locally
↾t Locally ↾t |
17 | | simpl 473 |
. . . . . . . . . . 11
|
18 | 16, 17 | syl6bi 243 |
. . . . . . . . . 10
Locally Locally
↾t Locally ↾t
|
19 | | simprl 794 |
. . . . . . . . . . . . 13
Locally Locally
↾t Locally
↾t ↾t |
20 | | simprr1 1109 |
. . . . . . . . . . . . . . 15
Locally Locally
↾t Locally
↾t ↾t |
21 | | simprr1 1109 |
. . . . . . . . . . . . . . . 16
Locally Locally
↾t Locally |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . 15
Locally Locally
↾t Locally
↾t ↾t |
23 | 20, 22 | sstrd 3613 |
. . . . . . . . . . . . . 14
Locally Locally
↾t Locally
↾t ↾t |
24 | | selpw 4165 |
. . . . . . . . . . . . . 14
|
25 | 23, 24 | sylibr 224 |
. . . . . . . . . . . . 13
Locally Locally
↾t Locally
↾t ↾t |
26 | 19, 25 | elind 3798 |
. . . . . . . . . . . 12
Locally Locally
↾t Locally
↾t ↾t |
27 | | simprr2 1110 |
. . . . . . . . . . . 12
Locally Locally
↾t Locally
↾t ↾t |
28 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
Locally Locally
↾t Locally
↾t ↾t |
29 | | simplrl 800 |
. . . . . . . . . . . . . 14
Locally Locally
↾t Locally
↾t ↾t |
30 | | restabs 20969 |
. . . . . . . . . . . . . 14
↾t
↾t
↾t |
31 | 28, 20, 29, 30 | syl3anc 1326 |
. . . . . . . . . . . . 13
Locally Locally
↾t Locally
↾t ↾t
↾t
↾t
↾t |
32 | | simprr3 1111 |
. . . . . . . . . . . . 13
Locally Locally
↾t Locally
↾t ↾t
↾t
↾t |
33 | 31, 32 | eqeltrrd 2702 |
. . . . . . . . . . . 12
Locally Locally
↾t Locally
↾t ↾t ↾t |
34 | 26, 27, 33 | jca32 558 |
. . . . . . . . . . 11
Locally Locally
↾t Locally
↾t ↾t ↾t |
35 | 34 | ex 450 |
. . . . . . . . . 10
Locally Locally
↾t Locally ↾t ↾t ↾t |
36 | 18, 35 | syland 498 |
. . . . . . . . 9
Locally Locally
↾t Locally ↾t
↾t ↾t
↾t |
37 | 36 | reximdv2 3014 |
. . . . . . . 8
Locally Locally
↾t Locally
↾t
↾t
↾t ↾t |
38 | 14, 37 | mpd 15 |
. . . . . . 7
Locally Locally
↾t Locally ↾t |
39 | 2, 38 | rexlimddv 3035 |
. . . . . 6
Locally
Locally
↾t |
40 | 39 | 3expb 1266 |
. . . . 5
Locally
Locally
↾t |
41 | 40 | ralrimivva 2971 |
. . . 4
Locally Locally
↾t |
42 | | islly 21271 |
. . . 4
Locally
↾t |
43 | 1, 41, 42 | sylanbrc 698 |
. . 3
Locally Locally
Locally |
44 | 43 | ssriv 3607 |
. 2
Locally Locally
Locally |
45 | | llyrest 21288 |
. . . . 5
Locally
↾t Locally |
46 | 45 | adantl 482 |
. . . 4
Locally
↾t Locally |
47 | | llytop 21275 |
. . . . . 6
Locally
|
48 | 47 | ssriv 3607 |
. . . . 5
Locally |
49 | 48 | a1i 11 |
. . . 4
Locally
|
50 | 46, 49 | restlly 21286 |
. . 3
Locally
Locally Locally |
51 | 50 | trud 1493 |
. 2
Locally Locally Locally |
52 | 44, 51 | eqssi 3619 |
1
Locally Locally
Locally |