Step | Hyp | Ref
| Expression |
1 | | 1stctop 21246 |
. . 3
|
2 | | resttop 20964 |
. . 3
↾t |
3 | 1, 2 | sylan 488 |
. 2
↾t |
4 | | eqid 2622 |
. . . . . . . 8
|
5 | 4 | restuni2 20971 |
. . . . . . 7
↾t |
6 | 1, 5 | sylan 488 |
. . . . . 6
↾t |
7 | 6 | eleq2d 2687 |
. . . . 5
↾t |
8 | 7 | biimpar 502 |
. . . 4
↾t
|
9 | | simpl 473 |
. . . . . 6
|
10 | | inss2 3834 |
. . . . . . 7
|
11 | 10 | sseli 3599 |
. . . . . 6
|
12 | 4 | 1stcclb 21247 |
. . . . . 6
|
13 | 9, 11, 12 | syl2an 494 |
. . . . 5
|
14 | | simplll 798 |
. . . . . . . 8
|
15 | | elpwi 4168 |
. . . . . . . . 9
|
16 | 15 | ad2antrl 764 |
. . . . . . . 8
|
17 | | ssrest 20980 |
. . . . . . . 8
↾t ↾t |
18 | 14, 16, 17 | syl2anc 693 |
. . . . . . 7
↾t
↾t |
19 | | ovex 6678 |
. . . . . . . 8
↾t |
20 | 19 | elpw2 4828 |
. . . . . . 7
↾t
↾t
↾t
↾t |
21 | 18, 20 | sylibr 224 |
. . . . . 6
↾t ↾t |
22 | | vex 3203 |
. . . . . . . 8
|
23 | | simpllr 799 |
. . . . . . . 8
|
24 | | restval 16087 |
. . . . . . . 8
↾t |
25 | 22, 23, 24 | sylancr 695 |
. . . . . . 7
↾t |
26 | | simprrl 804 |
. . . . . . . 8
|
27 | | 1stcrestlem 21255 |
. . . . . . . 8
|
28 | 26, 27 | syl 17 |
. . . . . . 7
|
29 | 25, 28 | eqbrtrd 4675 |
. . . . . 6
↾t |
30 | 1 | ad3antrrr 766 |
. . . . . . . . 9
|
31 | | elrest 16088 |
. . . . . . . . 9
↾t
|
32 | 30, 23, 31 | syl2anc 693 |
. . . . . . . 8
↾t
|
33 | | r19.29 3072 |
. . . . . . . . . . . 12
|
34 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
35 | 34 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
36 | 35 | ancld 576 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
37 | | elin 3796 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | 36, 37 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | | ssrin 3838 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
|
41 | 38, 40 | anim12d 586 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 41 | reximdv 3016 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 43 | inex1 4799 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . 22
|
47 | | elrest 16088 |
. . . . . . . . . . . . . . . . . . . . . 22
↾t
|
48 | 22, 46, 47 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
↾t
|
49 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
50 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 49, 50 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 45, 48, 52 | rexxfr2d 4883 |
. . . . . . . . . . . . . . . . . . . 20
↾t
|
54 | 42, 53 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . 19
↾t |
55 | 54 | expr 643 |
. . . . . . . . . . . . . . . . . 18
↾t |
56 | 55 | com23 86 |
. . . . . . . . . . . . . . . . 17
↾t |
57 | 56 | imim2d 57 |
. . . . . . . . . . . . . . . 16
↾t |
58 | 57 | imp4b 613 |
. . . . . . . . . . . . . . 15
↾t |
59 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
|
60 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
61 | 59, 60 | syl6bb 276 |
. . . . . . . . . . . . . . . 16
|
62 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . 18
|
63 | 62 | anbi2d 740 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
↾t
↾t |
65 | 61, 64 | imbi12d 334 |
. . . . . . . . . . . . . . 15
↾t
↾t |
66 | 58, 65 | syl5ibrcom 237 |
. . . . . . . . . . . . . 14
↾t |
67 | 66 | expimpd 629 |
. . . . . . . . . . . . 13
↾t |
68 | 67 | rexlimdva 3031 |
. . . . . . . . . . . 12
↾t |
69 | 33, 68 | syl5 34 |
. . . . . . . . . . 11
↾t |
70 | 69 | expd 452 |
. . . . . . . . . 10
↾t |
71 | 70 | impr 649 |
. . . . . . . . 9
↾t |
72 | 71 | adantrrl 760 |
. . . . . . . 8
↾t |
73 | 32, 72 | sylbid 230 |
. . . . . . 7
↾t
↾t |
74 | 73 | ralrimiv 2965 |
. . . . . 6
↾t
↾t |
75 | | breq1 4656 |
. . . . . . . 8
↾t ↾t |
76 | | rexeq 3139 |
. . . . . . . . . 10
↾t
↾t |
77 | 76 | imbi2d 330 |
. . . . . . . . 9
↾t
↾t |
78 | 77 | ralbidv 2986 |
. . . . . . . 8
↾t
↾t
↾t
↾t |
79 | 75, 78 | anbi12d 747 |
. . . . . . 7
↾t
↾t
↾t
↾t
↾t |
80 | 79 | rspcev 3309 |
. . . . . 6
↾t
↾t
↾t ↾t
↾t
↾t ↾t
|
81 | 21, 29, 74, 80 | syl12anc 1324 |
. . . . 5
↾t ↾t
|
82 | 13, 81 | rexlimddv 3035 |
. . . 4
↾t ↾t
|
83 | 8, 82 | syldan 487 |
. . 3
↾t
↾t
↾t
|
84 | 83 | ralrimiva 2966 |
. 2
↾t
↾t
↾t
|
85 | | eqid 2622 |
. . 3
↾t
↾t |
86 | 85 | is1stc2 21245 |
. 2
↾t
↾t
↾t ↾t ↾t
|
87 | 3, 84, 86 | sylanbrc 698 |
1
↾t |