Step | Hyp | Ref
| Expression |
1 | | xpcval.t |
. 2
c |
2 | | df-xpc 16812 |
. . . 4
c
comp comp comp |
3 | 2 | a1i 11 |
. . 3
c
comp comp comp |
4 | | fvex 6201 |
. . . . . 6
|
5 | | fvex 6201 |
. . . . . 6
|
6 | 4, 5 | xpex 6962 |
. . . . 5
|
7 | 6 | a1i 11 |
. . . 4
|
8 | | simprl 794 |
. . . . . . . 8
|
9 | 8 | fveq2d 6195 |
. . . . . . 7
|
10 | | xpcval.x |
. . . . . . 7
|
11 | 9, 10 | syl6eqr 2674 |
. . . . . 6
|
12 | | simprr 796 |
. . . . . . . 8
|
13 | 12 | fveq2d 6195 |
. . . . . . 7
|
14 | | xpcval.y |
. . . . . . 7
|
15 | 13, 14 | syl6eqr 2674 |
. . . . . 6
|
16 | 11, 15 | xpeq12d 5140 |
. . . . 5
|
17 | | xpcval.b |
. . . . . 6
|
18 | 17 | adantr 481 |
. . . . 5
|
19 | 16, 18 | eqtr4d 2659 |
. . . 4
|
20 | | vex 3203 |
. . . . . . 7
|
21 | 20, 20 | mpt2ex 7247 |
. . . . . 6
|
22 | 21 | a1i 11 |
. . . . 5
|
23 | | simpr 477 |
. . . . . . 7
|
24 | | simplrl 800 |
. . . . . . . . . . 11
|
25 | 24 | fveq2d 6195 |
. . . . . . . . . 10
|
26 | | xpcval.h |
. . . . . . . . . 10
|
27 | 25, 26 | syl6eqr 2674 |
. . . . . . . . 9
|
28 | 27 | oveqd 6667 |
. . . . . . . 8
|
29 | | simplrr 801 |
. . . . . . . . . . 11
|
30 | 29 | fveq2d 6195 |
. . . . . . . . . 10
|
31 | | xpcval.j |
. . . . . . . . . 10
|
32 | 30, 31 | syl6eqr 2674 |
. . . . . . . . 9
|
33 | 32 | oveqd 6667 |
. . . . . . . 8
|
34 | 28, 33 | xpeq12d 5140 |
. . . . . . 7
|
35 | 23, 23, 34 | mpt2eq123dv 6717 |
. . . . . 6
|
36 | | xpcval.k |
. . . . . . 7
|
37 | 36 | ad2antrr 762 |
. . . . . 6
|
38 | 35, 37 | eqtr4d 2659 |
. . . . 5
|
39 | | simplr 792 |
. . . . . . 7
|
40 | 39 | opeq2d 4409 |
. . . . . 6
|
41 | | simpr 477 |
. . . . . . 7
|
42 | 41 | opeq2d 4409 |
. . . . . 6
|
43 | 39, 39 | xpeq12d 5140 |
. . . . . . . . 9
|
44 | 41 | oveqd 6667 |
. . . . . . . . . 10
|
45 | 41 | fveq1d 6193 |
. . . . . . . . . 10
|
46 | 24 | adantr 481 |
. . . . . . . . . . . . . . 15
|
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . . . 14
comp comp |
48 | | xpcval.o1 |
. . . . . . . . . . . . . 14
comp |
49 | 47, 48 | syl6eqr 2674 |
. . . . . . . . . . . . 13
comp |
50 | 49 | oveqd 6667 |
. . . . . . . . . . . 12
comp |
51 | 50 | oveqd 6667 |
. . . . . . . . . . 11
comp |
52 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
|
53 | 52 | fveq2d 6195 |
. . . . . . . . . . . . . 14
comp comp |
54 | | xpcval.o2 |
. . . . . . . . . . . . . 14
comp |
55 | 53, 54 | syl6eqr 2674 |
. . . . . . . . . . . . 13
comp |
56 | 55 | oveqd 6667 |
. . . . . . . . . . . 12
comp |
57 | 56 | oveqd 6667 |
. . . . . . . . . . 11
comp |
58 | 51, 57 | opeq12d 4410 |
. . . . . . . . . 10
comp comp |
59 | 44, 45, 58 | mpt2eq123dv 6717 |
. . . . . . . . 9
comp comp |
60 | 43, 39, 59 | mpt2eq123dv 6717 |
. . . . . . . 8
comp comp |
61 | | xpcval.o |
. . . . . . . . 9
|
62 | 61 | ad3antrrr 766 |
. . . . . . . 8
|
63 | 60, 62 | eqtr4d 2659 |
. . . . . . 7
comp comp |
64 | 63 | opeq2d 4409 |
. . . . . 6
comp comp comp comp |
65 | 40, 42, 64 | tpeq123d 4283 |
. . . . 5
comp comp comp
comp |
66 | 22, 38, 65 | csbied2 3561 |
. . . 4
comp comp comp
comp |
67 | 7, 19, 66 | csbied2 3561 |
. . 3
comp comp comp
comp |
68 | | xpcval.c |
. . . 4
|
69 | | elex 3212 |
. . . 4
|
70 | 68, 69 | syl 17 |
. . 3
|
71 | | xpcval.d |
. . . 4
|
72 | | elex 3212 |
. . . 4
|
73 | 71, 72 | syl 17 |
. . 3
|
74 | | tpex 6957 |
. . . 4
comp |
75 | 74 | a1i 11 |
. . 3
comp |
76 | 3, 67, 70, 73, 75 | ovmpt2d 6788 |
. 2
c comp |
77 | 1, 76 | syl5eq 2668 |
1
comp |