Step | Hyp | Ref
| Expression |
1 | | df-cur 7393 |
. 2
curry |
2 | | mpt2curryd.c |
. . . . . . 7
|
3 | | mpt2curryd.f |
. . . . . . . 8
|
4 | 3 | dmmpt2ga 7242 |
. . . . . . 7
|
5 | 2, 4 | syl 17 |
. . . . . 6
|
6 | 5 | dmeqd 5326 |
. . . . 5
|
7 | | mpt2curryd.n |
. . . . . 6
|
8 | | dmxp 5344 |
. . . . . 6
|
9 | 7, 8 | syl 17 |
. . . . 5
|
10 | 6, 9 | eqtrd 2656 |
. . . 4
|
11 | 10 | mpteq1d 4738 |
. . 3
|
12 | | df-mpt 4730 |
. . . . 5
|
13 | 3 | mpt2fun 6762 |
. . . . . . . 8
|
14 | | funbrfv2b 6240 |
. . . . . . . 8
|
15 | 13, 14 | mp1i 13 |
. . . . . . 7
|
16 | 5 | adantr 481 |
. . . . . . . . . 10
|
17 | 16 | eleq2d 2687 |
. . . . . . . . 9
|
18 | | opelxp 5146 |
. . . . . . . . 9
|
19 | 17, 18 | syl6bb 276 |
. . . . . . . 8
|
20 | 19 | anbi1d 741 |
. . . . . . 7
|
21 | | an32 839 |
. . . . . . . . 9
|
22 | | ancom 466 |
. . . . . . . . 9
|
23 | 21, 22 | bitri 264 |
. . . . . . . 8
|
24 | | ibar 525 |
. . . . . . . . . . . . 13
|
25 | 24 | bicomd 213 |
. . . . . . . . . . . 12
|
26 | 25 | adantl 482 |
. . . . . . . . . . 11
|
27 | 26 | adantr 481 |
. . . . . . . . . 10
|
28 | | df-ov 6653 |
. . . . . . . . . . . . 13
|
29 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
30 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
31 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . 18
|
32 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . 18
|
33 | 31, 32 | nfcsb 3551 |
. . . . . . . . . . . . . . . . 17
|
34 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . 17
|
35 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
36 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
37 | 35, 36 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . 17
|
38 | 29, 30, 33, 34, 37 | cbvmpt2 6734 |
. . . . . . . . . . . . . . . 16
|
39 | 3, 38 | eqtri 2644 |
. . . . . . . . . . . . . . 15
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
|
41 | 35 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41 | equcoms 1947 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | csbeq2dv 3992 |
. . . . . . . . . . . . . . . 16
|
44 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | equcoms 1947 |
. . . . . . . . . . . . . . . 16
|
47 | 43, 46 | sylan9eq 2676 |
. . . . . . . . . . . . . . 15
|
48 | 47 | adantl 482 |
. . . . . . . . . . . . . 14
|
49 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . . 14
|
51 | | simpr 477 |
. . . . . . . . . . . . . 14
|
52 | | rsp2 2936 |
. . . . . . . . . . . . . . . 16
|
53 | 2, 52 | syl 17 |
. . . . . . . . . . . . . . 15
|
54 | 53 | impl 650 |
. . . . . . . . . . . . . 14
|
55 | 40, 48, 50, 51, 54 | ovmpt2d 6788 |
. . . . . . . . . . . . 13
|
56 | 28, 55 | syl5eqr 2670 |
. . . . . . . . . . . 12
|
57 | 56 | eqeq1d 2624 |
. . . . . . . . . . 11
|
58 | | eqcom 2629 |
. . . . . . . . . . 11
|
59 | 57, 58 | syl6bb 276 |
. . . . . . . . . 10
|
60 | 27, 59 | bitrd 268 |
. . . . . . . . 9
|
61 | 60 | pm5.32da 673 |
. . . . . . . 8
|
62 | 23, 61 | syl5bb 272 |
. . . . . . 7
|
63 | 15, 20, 62 | 3bitrrd 295 |
. . . . . 6
|
64 | 63 | opabbidv 4716 |
. . . . 5
|
65 | 12, 64 | syl5req 2669 |
. . . 4
|
66 | 65 | mpteq2dva 4744 |
. . 3
|
67 | 11, 66 | eqtrd 2656 |
. 2
|
68 | 1, 67 | syl5eq 2668 |
1
curry |