Step | Hyp | Ref
| Expression |
1 | | wrd2f1tovbij.d |
. . 3
Word |
2 | | wrd2f1tovbij.r |
. . 3
|
3 | | wrd2f1tovbij.f |
. . 3
|
4 | 1, 2, 3 | wwlktovf 13699 |
. 2
|
5 | | fveq1 6190 |
. . . . . 6
|
6 | | fvex 6201 |
. . . . . 6
|
7 | 5, 3, 6 | fvmpt 6282 |
. . . . 5
|
8 | | fveq1 6190 |
. . . . . 6
|
9 | | fvex 6201 |
. . . . . 6
|
10 | 8, 3, 9 | fvmpt 6282 |
. . . . 5
|
11 | 7, 10 | eqeqan12d 2638 |
. . . 4
|
12 | | fveq2 6191 |
. . . . . . . 8
|
13 | 12 | eqeq1d 2624 |
. . . . . . 7
|
14 | | fveq1 6190 |
. . . . . . . 8
|
15 | 14 | eqeq1d 2624 |
. . . . . . 7
|
16 | | fveq1 6190 |
. . . . . . . . 9
|
17 | 14, 16 | preq12d 4276 |
. . . . . . . 8
|
18 | 17 | eleq1d 2686 |
. . . . . . 7
|
19 | 13, 15, 18 | 3anbi123d 1399 |
. . . . . 6
|
20 | 19, 1 | elrab2 3366 |
. . . . 5
Word
|
21 | | fveq2 6191 |
. . . . . . . 8
|
22 | 21 | eqeq1d 2624 |
. . . . . . 7
|
23 | | fveq1 6190 |
. . . . . . . 8
|
24 | 23 | eqeq1d 2624 |
. . . . . . 7
|
25 | | fveq1 6190 |
. . . . . . . . 9
|
26 | 23, 25 | preq12d 4276 |
. . . . . . . 8
|
27 | 26 | eleq1d 2686 |
. . . . . . 7
|
28 | 22, 24, 27 | 3anbi123d 1399 |
. . . . . 6
|
29 | 28, 1 | elrab2 3366 |
. . . . 5
Word
|
30 | | simp1 1061 |
. . . . . . . . . 10
|
31 | 30 | adantl 482 |
. . . . . . . . 9
Word |
32 | | simp1 1061 |
. . . . . . . . . . 11
|
33 | 32 | eqcomd 2628 |
. . . . . . . . . 10
|
34 | 33 | adantl 482 |
. . . . . . . . 9
Word |
35 | 31, 34 | sylan9eq 2676 |
. . . . . . . 8
Word Word |
36 | 35 | adantr 481 |
. . . . . . 7
Word Word
|
37 | | simp2 1062 |
. . . . . . . . . . 11
|
38 | 37 | adantl 482 |
. . . . . . . . . 10
Word |
39 | | simp2 1062 |
. . . . . . . . . . . 12
|
40 | 39 | eqcomd 2628 |
. . . . . . . . . . 11
|
41 | 40 | adantl 482 |
. . . . . . . . . 10
Word |
42 | 38, 41 | sylan9eq 2676 |
. . . . . . . . 9
Word Word |
43 | 42 | adantr 481 |
. . . . . . . 8
Word Word
|
44 | | simpr 477 |
. . . . . . . 8
Word Word
|
45 | | oveq2 6658 |
. . . . . . . . . . . . 13
..^ ..^ |
46 | | fzo0to2pr 12553 |
. . . . . . . . . . . . 13
..^ |
47 | 45, 46 | syl6eq 2672 |
. . . . . . . . . . . 12
..^ |
48 | 47 | raleqdv 3144 |
. . . . . . . . . . 11
..^ |
49 | | c0ex 10034 |
. . . . . . . . . . . 12
|
50 | | 1ex 10035 |
. . . . . . . . . . . 12
|
51 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
52 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
53 | 51, 52 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
54 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
55 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
56 | 54, 55 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
57 | 49, 50, 53, 56 | ralpr 4238 |
. . . . . . . . . . 11
|
58 | 48, 57 | syl6bb 276 |
. . . . . . . . . 10
..^
|
59 | 58 | 3ad2ant1 1082 |
. . . . . . . . 9
..^
|
60 | 59 | ad3antlr 767 |
. . . . . . . 8
Word Word
..^
|
61 | 43, 44, 60 | mpbir2and 957 |
. . . . . . 7
Word Word
..^ |
62 | | simpl 473 |
. . . . . . . . . 10
Word Word |
63 | | simpl 473 |
. . . . . . . . . 10
Word Word |
64 | 62, 63 | anim12i 590 |
. . . . . . . . 9
Word Word Word
Word |
65 | 64 | adantr 481 |
. . . . . . . 8
Word Word
Word
Word |
66 | | eqwrd 13346 |
. . . . . . . 8
Word
Word
..^ |
67 | 65, 66 | syl 17 |
. . . . . . 7
Word Word
..^ |
68 | 36, 61, 67 | mpbir2and 957 |
. . . . . 6
Word Word
|
69 | 68 | ex 450 |
. . . . 5
Word Word |
70 | 20, 29, 69 | syl2anb 496 |
. . . 4
|
71 | 11, 70 | sylbid 230 |
. . 3
|
72 | 71 | rgen2a 2977 |
. 2
|
73 | | dff13 6512 |
. 2
|
74 | 4, 72, 73 | mpbir2an 955 |
1
|