Step | Hyp | Ref
| Expression |
1 | | ssrab2 3687 |
. . . . . . . 8
|
2 | | sseq1 3626 |
. . . . . . . 8
|
3 | 1, 2 | mpbiri 248 |
. . . . . . 7
|
4 | 3 | a1i 11 |
. . . . . 6
|
5 | | eqid 2622 |
. . . . . . . . . 10
|
6 | | eqid 2622 |
. . . . . . . . . 10
|
7 | 5, 6 | atbase 34576 |
. . . . . . . . 9
|
8 | 5, 6 | atbase 34576 |
. . . . . . . . 9
|
9 | 7, 8 | anim12i 590 |
. . . . . . . 8
|
10 | | eqid 2622 |
. . . . . . . . . 10
|
11 | 5, 10 | latjcl 17051 |
. . . . . . . . 9
|
12 | 11 | 3expb 1266 |
. . . . . . . 8
|
13 | 9, 12 | sylan2 491 |
. . . . . . 7
|
14 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . 19
|
15 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
|
16 | 15 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
|
17 | 5, 6 | atbase 34576 |
. . . . . . . . . . . . . . . . . . . . 21
|
18 | 17 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . 20
|
19 | 16, 18 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 14, 19 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
|
21 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . 19
|
22 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
|
23 | 22 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
|
24 | 5, 6 | atbase 34576 |
. . . . . . . . . . . . . . . . . . . . 21
|
25 | 24 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | 23, 25 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 21, 26 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
|
28 | 20, 27 | anim12d 586 |
. . . . . . . . . . . . . . . . 17
|
29 | | an4 865 |
. . . . . . . . . . . . . . . . 17
|
30 | 28, 29 | syl6ib 241 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | imp 445 |
. . . . . . . . . . . . . . 15
|
32 | 31 | anim2i 593 |
. . . . . . . . . . . . . 14
|
33 | 32 | anassrs 680 |
. . . . . . . . . . . . 13
|
34 | 5, 6 | atbase 34576 |
. . . . . . . . . . . . 13
|
35 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
36 | 5, 35, 10 | latjle12 17062 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | 36 | biimpd 219 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 37 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . 18
|
39 | 38 | impd 447 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | com23 86 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | imp43 621 |
. . . . . . . . . . . . . . 15
|
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
|
43 | 5, 10 | latjcl 17051 |
. . . . . . . . . . . . . . . . . 18
|
44 | 43 | 3expib 1268 |
. . . . . . . . . . . . . . . . 17
|
45 | 5, 35 | lattr 17056 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 45 | 3exp2 1285 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | com24 95 |
. . . . . . . . . . . . . . . . 17
|
48 | 44, 47 | syl5d 73 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | imp41 619 |
. . . . . . . . . . . . . . 15
|
50 | 49 | adantlrr 757 |
. . . . . . . . . . . . . 14
|
51 | 42, 50 | mpan2d 710 |
. . . . . . . . . . . . 13
|
52 | 33, 34, 51 | syl2an 494 |
. . . . . . . . . . . 12
|
53 | | simpr 477 |
. . . . . . . . . . . 12
|
54 | 52, 53 | jctild 566 |
. . . . . . . . . . 11
|
55 | | eleq2 2690 |
. . . . . . . . . . . . 13
|
56 | | breq1 4656 |
. . . . . . . . . . . . . 14
|
57 | 56 | elrab 3363 |
. . . . . . . . . . . . 13
|
58 | 55, 57 | syl6bb 276 |
. . . . . . . . . . . 12
|
59 | 58 | ad3antlr 767 |
. . . . . . . . . . 11
|
60 | 54, 59 | sylibrd 249 |
. . . . . . . . . 10
|
61 | 60 | ralrimiva 2966 |
. . . . . . . . 9
|
62 | 61 | ralrimivva 2971 |
. . . . . . . 8
|
63 | 62 | ex 450 |
. . . . . . 7
|
64 | 13, 63 | syldan 487 |
. . . . . 6
|
65 | 4, 64 | jcad 555 |
. . . . 5
|
66 | 65 | adantld 483 |
. . . 4
|
67 | 66 | rexlimdvva 3038 |
. . 3
|
68 | | linepsub.n |
. . . 4
|
69 | 35, 10, 6, 68 | isline 35025 |
. . 3
|
70 | | linepsub.s |
. . . 4
|
71 | 35, 10, 6, 70 | ispsubsp 35031 |
. . 3
|
72 | 67, 69, 71 | 3imtr4d 283 |
. 2
|
73 | 72 | imp 445 |
1
|