Step | Hyp | Ref
| Expression |
1 | | dmres 5419 |
. . . . 5
|
2 | 1 | imaeq2i 5464 |
. . . 4
|
3 | | imadmres 5627 |
. . . 4
|
4 | 2, 3 | eqtr3i 2646 |
. . 3
|
5 | 4 | sseq2i 3630 |
. 2
|
6 | | ssrab2 3687 |
. . . 4
|
7 | | ssel2 3598 |
. . . . . . . . 9
|
8 | 7 | adantll 750 |
. . . . . . . 8
|
9 | | fvelima 6248 |
. . . . . . . . . . . 12
|
10 | 9 | ex 450 |
. . . . . . . . . . 11
|
11 | 10 | adantr 481 |
. . . . . . . . . 10
|
12 | | eleq1a 2696 |
. . . . . . . . . . . . . . . 16
|
13 | 12 | anim2d 589 |
. . . . . . . . . . . . . . 15
|
14 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
15 | 14 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
16 | 15 | elrab 3363 |
. . . . . . . . . . . . . . 15
|
17 | 13, 16 | syl6ibr 242 |
. . . . . . . . . . . . . 14
|
18 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
|
20 | 17, 19 | jcad 555 |
. . . . . . . . . . . . 13
|
21 | 20 | reximdv2 3014 |
. . . . . . . . . . . 12
|
22 | 21 | adantl 482 |
. . . . . . . . . . 11
|
23 | | funfn 5918 |
. . . . . . . . . . . . 13
|
24 | | inss2 3834 |
. . . . . . . . . . . . . . 15
|
25 | 6, 24 | sstri 3612 |
. . . . . . . . . . . . . 14
|
26 | | fvelimab 6253 |
. . . . . . . . . . . . . 14
|
27 | 25, 26 | mpan2 707 |
. . . . . . . . . . . . 13
|
28 | 23, 27 | sylbi 207 |
. . . . . . . . . . . 12
|
29 | 28 | adantr 481 |
. . . . . . . . . . 11
|
30 | 22, 29 | sylibrd 249 |
. . . . . . . . . 10
|
31 | 11, 30 | syld 47 |
. . . . . . . . 9
|
32 | 31 | adantlr 751 |
. . . . . . . 8
|
33 | 8, 32 | mpd 15 |
. . . . . . 7
|
34 | 33 | ex 450 |
. . . . . 6
|
35 | | fvelima 6248 |
. . . . . . . . 9
|
36 | 35 | ex 450 |
. . . . . . . 8
|
37 | | eleq1 2689 |
. . . . . . . . . . . 12
|
38 | 37 | biimpcd 239 |
. . . . . . . . . . 11
|
39 | 38 | adantl 482 |
. . . . . . . . . 10
|
40 | 16, 39 | sylbi 207 |
. . . . . . . . 9
|
41 | 40 | rexlimiv 3027 |
. . . . . . . 8
|
42 | 36, 41 | syl6 35 |
. . . . . . 7
|
43 | 42 | adantr 481 |
. . . . . 6
|
44 | 34, 43 | impbid 202 |
. . . . 5
|
45 | 44 | eqrdv 2620 |
. . . 4
|
46 | | ssimaex.1 |
. . . . . . 7
|
47 | 46 | inex1 4799 |
. . . . . 6
|
48 | 47 | rabex 4813 |
. . . . 5
|
49 | | sseq1 3626 |
. . . . . 6
|
50 | | imaeq2 5462 |
. . . . . . 7
|
51 | 50 | eqeq2d 2632 |
. . . . . 6
|
52 | 49, 51 | anbi12d 747 |
. . . . 5
|
53 | 48, 52 | spcev 3300 |
. . . 4
|
54 | 6, 45, 53 | sylancr 695 |
. . 3
|
55 | | inss1 3833 |
. . . . . 6
|
56 | | sstr 3611 |
. . . . . 6
|
57 | 55, 56 | mpan2 707 |
. . . . 5
|
58 | 57 | anim1i 592 |
. . . 4
|
59 | 58 | eximi 1762 |
. . 3
|
60 | 54, 59 | syl 17 |
. 2
|
61 | 5, 60 | sylan2br 493 |
1
|