Step | Hyp | Ref
| Expression |
1 | | natfval.1 |
. . . . . 6
Nat |
2 | | natfval.b |
. . . . . 6
|
3 | | natfval.h |
. . . . . 6
|
4 | | natfval.j |
. . . . . 6
|
5 | | natfval.o |
. . . . . 6
comp |
6 | 1, 2, 3, 4, 5 | natfval 16606 |
. . . . 5
|
7 | 6 | a1i 11 |
. . . 4
|
8 | | fvexd 6203 |
. . . . 5
|
9 | | simprl 794 |
. . . . . . 7
|
10 | 9 | fveq2d 6195 |
. . . . . 6
|
11 | | relfunc 16522 |
. . . . . . . . 9
|
12 | | isnat.f |
. . . . . . . . 9
|
13 | | brrelex12 5155 |
. . . . . . . . 9
|
14 | 11, 12, 13 | sylancr 695 |
. . . . . . . 8
|
15 | | op1stg 7180 |
. . . . . . . 8
|
16 | 14, 15 | syl 17 |
. . . . . . 7
|
17 | 16 | adantr 481 |
. . . . . 6
|
18 | 10, 17 | eqtrd 2656 |
. . . . 5
|
19 | | fvexd 6203 |
. . . . . 6
|
20 | | simplrr 801 |
. . . . . . . 8
|
21 | 20 | fveq2d 6195 |
. . . . . . 7
|
22 | | isnat.g |
. . . . . . . . . 10
|
23 | | brrelex12 5155 |
. . . . . . . . . 10
|
24 | 11, 22, 23 | sylancr 695 |
. . . . . . . . 9
|
25 | | op1stg 7180 |
. . . . . . . . 9
|
26 | 24, 25 | syl 17 |
. . . . . . . 8
|
27 | 26 | ad2antrr 762 |
. . . . . . 7
|
28 | 21, 27 | eqtrd 2656 |
. . . . . 6
|
29 | | simplr 792 |
. . . . . . . . . 10
|
30 | 29 | fveq1d 6193 |
. . . . . . . . 9
|
31 | | simpr 477 |
. . . . . . . . . 10
|
32 | 31 | fveq1d 6193 |
. . . . . . . . 9
|
33 | 30, 32 | oveq12d 6668 |
. . . . . . . 8
|
34 | 33 | ixpeq2dv 7924 |
. . . . . . 7
|
35 | 29 | fveq1d 6193 |
. . . . . . . . . . . . 13
|
36 | 30, 35 | opeq12d 4410 |
. . . . . . . . . . . 12
|
37 | 31 | fveq1d 6193 |
. . . . . . . . . . . 12
|
38 | 36, 37 | oveq12d 6668 |
. . . . . . . . . . 11
|
39 | | eqidd 2623 |
. . . . . . . . . . 11
|
40 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
42 | | op2ndg 7181 |
. . . . . . . . . . . . . . . 16
|
43 | 14, 42 | syl 17 |
. . . . . . . . . . . . . . 15
|
44 | 43 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
45 | 41, 44 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
46 | 45 | oveqd 6667 |
. . . . . . . . . . . 12
|
47 | 46 | fveq1d 6193 |
. . . . . . . . . . 11
|
48 | 38, 39, 47 | oveq123d 6671 |
. . . . . . . . . 10
|
49 | 30, 32 | opeq12d 4410 |
. . . . . . . . . . . 12
|
50 | 49, 37 | oveq12d 6668 |
. . . . . . . . . . 11
|
51 | 20 | adantr 481 |
. . . . . . . . . . . . . . 15
|
52 | 51 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
53 | | op2ndg 7181 |
. . . . . . . . . . . . . . . 16
|
54 | 24, 53 | syl 17 |
. . . . . . . . . . . . . . 15
|
55 | 54 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
|
56 | 52, 55 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
57 | 56 | oveqd 6667 |
. . . . . . . . . . . 12
|
58 | 57 | fveq1d 6193 |
. . . . . . . . . . 11
|
59 | | eqidd 2623 |
. . . . . . . . . . 11
|
60 | 50, 58, 59 | oveq123d 6671 |
. . . . . . . . . 10
|
61 | 48, 60 | eqeq12d 2637 |
. . . . . . . . 9
|
62 | 61 | ralbidv 2986 |
. . . . . . . 8
|
63 | 62 | 2ralbidv 2989 |
. . . . . . 7
|
64 | 34, 63 | rabeqbidv 3195 |
. . . . . 6
|
65 | 19, 28, 64 | csbied2 3561 |
. . . . 5
|
66 | 8, 18, 65 | csbied2 3561 |
. . . 4
|
67 | | df-br 4654 |
. . . . 5
|
68 | 12, 67 | sylib 208 |
. . . 4
|
69 | | df-br 4654 |
. . . . 5
|
70 | 22, 69 | sylib 208 |
. . . 4
|
71 | | ovex 6678 |
. . . . . . . 8
|
72 | 71 | rgenw 2924 |
. . . . . . 7
|
73 | | ixpexg 7932 |
. . . . . . 7
|
74 | 72, 73 | ax-mp 5 |
. . . . . 6
|
75 | 74 | rabex 4813 |
. . . . 5
|
76 | 75 | a1i 11 |
. . . 4
|
77 | 7, 66, 68, 70, 76 | ovmpt2d 6788 |
. . 3
|
78 | 77 | eleq2d 2687 |
. 2
|
79 | | fveq1 6190 |
. . . . . . 7
|
80 | 79 | oveq1d 6665 |
. . . . . 6
|
81 | | fveq1 6190 |
. . . . . . 7
|
82 | 81 | oveq2d 6666 |
. . . . . 6
|
83 | 80, 82 | eqeq12d 2637 |
. . . . 5
|
84 | 83 | ralbidv 2986 |
. . . 4
|
85 | 84 | 2ralbidv 2989 |
. . 3
|
86 | 85 | elrab 3363 |
. 2
|
87 | 78, 86 | syl6bb 276 |
1
|