Step | Hyp | Ref
| Expression |
1 | | ofccat.1 |
. . . . . . . . . . 11
Word |
2 | | wrdf 13310 |
. . . . . . . . . . 11
Word ..^ |
3 | | ffn 6045 |
. . . . . . . . . . 11
..^ ..^ |
4 | 1, 2, 3 | 3syl 18 |
. . . . . . . . . 10
..^ |
5 | | ofccat.3 |
. . . . . . . . . . . 12
Word |
6 | | wrdf 13310 |
. . . . . . . . . . . 12
Word ..^ |
7 | | ffn 6045 |
. . . . . . . . . . . 12
..^ ..^ |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . . . . 11
..^ |
9 | | ofccat.5 |
. . . . . . . . . . . . 13
|
10 | 9 | oveq2d 6666 |
. . . . . . . . . . . 12
..^ ..^ |
11 | 10 | fneq2d 5982 |
. . . . . . . . . . 11
..^
..^ |
12 | 8, 11 | mpbird 247 |
. . . . . . . . . 10
..^ |
13 | | ovexd 6680 |
. . . . . . . . . 10
..^ |
14 | | inidm 3822 |
. . . . . . . . . 10
..^ ..^ ..^ |
15 | 4, 12, 13, 13, 14 | offn 6908 |
. . . . . . . . 9
..^ |
16 | | hashfn 13164 |
. . . . . . . . 9
..^ ..^ |
17 | 15, 16 | syl 17 |
. . . . . . . 8
..^ |
18 | | wrdfin 13323 |
. . . . . . . . . 10
Word |
19 | | hashcl 13147 |
. . . . . . . . . 10
|
20 | 1, 18, 19 | 3syl 18 |
. . . . . . . . 9
|
21 | | hashfzo0 13217 |
. . . . . . . . 9
..^ |
22 | 20, 21 | syl 17 |
. . . . . . . 8
..^ |
23 | 17, 22 | eqtrd 2656 |
. . . . . . 7
|
24 | 23 | adantr 481 |
. . . . . 6
..^ |
25 | 24 | oveq2d 6666 |
. . . . 5
..^ ..^ ..^ |
26 | 25 | eleq2d 2687 |
. . . 4
..^ ..^
..^ |
27 | 4 | ad2antrr 762 |
. . . . 5
..^ ..^ ..^ |
28 | 12 | ad2antrr 762 |
. . . . 5
..^ ..^ ..^ |
29 | | ovexd 6680 |
. . . . 5
..^ ..^ ..^ |
30 | 26 | biimpa 501 |
. . . . 5
..^ ..^ ..^ |
31 | | fnfvof 6911 |
. . . . 5
..^ ..^ ..^ ..^ |
32 | 27, 28, 29, 30, 31 | syl22anc 1327 |
. . . 4
..^ ..^ |
33 | 23 | ad2antrr 762 |
. . . . . . 7
..^ ..^ |
34 | 33 | oveq2d 6666 |
. . . . . 6
..^ ..^ |
35 | 34 | fveq2d 6195 |
. . . . 5
..^ ..^ |
36 | | ofccat.2 |
. . . . . . . 8
Word |
37 | | wrdf 13310 |
. . . . . . . 8
Word ..^ |
38 | | ffn 6045 |
. . . . . . . 8
..^ ..^ |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . 7
..^ |
40 | 39 | ad2antrr 762 |
. . . . . 6
..^ ..^ ..^ |
41 | | ofccat.4 |
. . . . . . . . 9
Word |
42 | | wrdf 13310 |
. . . . . . . . 9
Word ..^ |
43 | | ffn 6045 |
. . . . . . . . 9
..^ ..^ |
44 | 41, 42, 43 | 3syl 18 |
. . . . . . . 8
..^ |
45 | | ofccat.6 |
. . . . . . . . . 10
|
46 | 45 | oveq2d 6666 |
. . . . . . . . 9
..^ ..^ |
47 | 46 | fneq2d 5982 |
. . . . . . . 8
..^
..^ |
48 | 44, 47 | mpbird 247 |
. . . . . . 7
..^ |
49 | 48 | ad2antrr 762 |
. . . . . 6
..^ ..^ ..^ |
50 | | ovexd 6680 |
. . . . . 6
..^ ..^ ..^ |
51 | | simplr 792 |
. . . . . . 7
..^ ..^ ..^ |
52 | | simpr 477 |
. . . . . . . 8
..^ ..^
..^ |
53 | 25 | adantr 481 |
. . . . . . . 8
..^ ..^ ..^ ..^ |
54 | 52, 53 | neleqtrd 2722 |
. . . . . . 7
..^ ..^
..^ |
55 | 20 | ad2antrr 762 |
. . . . . . . 8
..^ ..^ |
56 | 55 | nn0zd 11480 |
. . . . . . 7
..^ ..^ |
57 | | wrdfin 13323 |
. . . . . . . . . 10
Word |
58 | | hashcl 13147 |
. . . . . . . . . 10
|
59 | 36, 57, 58 | 3syl 18 |
. . . . . . . . 9
|
60 | 59 | ad2antrr 762 |
. . . . . . . 8
..^ ..^ |
61 | 60 | nn0zd 11480 |
. . . . . . 7
..^ ..^ |
62 | | fzocatel 12531 |
. . . . . . 7
..^
..^ ..^ |
63 | 51, 54, 56, 61, 62 | syl22anc 1327 |
. . . . . 6
..^ ..^ ..^ |
64 | | fnfvof 6911 |
. . . . . 6
..^ ..^ ..^ ..^ |
65 | 40, 49, 50, 63, 64 | syl22anc 1327 |
. . . . 5
..^ ..^ |
66 | 35, 65 | eqtrd 2656 |
. . . 4
..^ ..^ |
67 | 26, 32, 66 | ifbieq12d2 4119 |
. . 3
..^ ..^ ..^ |
68 | 67 | mpteq2dva 4744 |
. 2
..^ ..^ ..^ ..^ |
69 | | ovex 6678 |
. . . 4
|
70 | | ovex 6678 |
. . . 4
|
71 | | ccatfval 13358 |
. . . 4
++ ..^ ..^ |
72 | 69, 70, 71 | mp2an 708 |
. . 3
++ ..^ ..^ |
73 | | ovexd 6680 |
. . . . . . . . 9
..^ |
74 | | inidm 3822 |
. . . . . . . . 9
..^ ..^ ..^ |
75 | 39, 48, 73, 73, 74 | offn 6908 |
. . . . . . . 8
..^ |
76 | | hashfn 13164 |
. . . . . . . 8
..^ ..^ |
77 | 75, 76 | syl 17 |
. . . . . . 7
..^ |
78 | | hashfzo0 13217 |
. . . . . . . 8
..^ |
79 | 59, 78 | syl 17 |
. . . . . . 7
..^ |
80 | 77, 79 | eqtrd 2656 |
. . . . . 6
|
81 | 23, 80 | oveq12d 6668 |
. . . . 5
|
82 | 81 | oveq2d 6666 |
. . . 4
..^ ..^ |
83 | 82 | mpteq1d 4738 |
. . 3
..^ ..^ ..^ ..^ |
84 | 72, 83 | syl5eq 2668 |
. 2
++ ..^ ..^ |
85 | | ovexd 6680 |
. . . . 5
..^ |
86 | | fvex 6201 |
. . . . . . 7
|
87 | | fvex 6201 |
. . . . . . 7
|
88 | 86, 87 | ifex 4156 |
. . . . . 6
..^ |
89 | 88 | a1i 11 |
. . . . 5
..^ ..^ |
90 | | fvex 6201 |
. . . . . . 7
|
91 | | fvex 6201 |
. . . . . . 7
|
92 | 90, 91 | ifex 4156 |
. . . . . 6
..^ |
93 | 92 | a1i 11 |
. . . . 5
..^ ..^ |
94 | | ccatfval 13358 |
. . . . . 6
Word
Word ++ ..^ ..^ |
95 | 1, 36, 94 | syl2anc 693 |
. . . . 5
++ ..^ ..^ |
96 | | ccatfval 13358 |
. . . . . . 7
Word
Word ++ ..^ ..^ |
97 | 5, 41, 96 | syl2anc 693 |
. . . . . 6
++ ..^ ..^ |
98 | 9, 45 | oveq12d 6668 |
. . . . . . . 8
|
99 | 98 | oveq2d 6666 |
. . . . . . 7
..^ ..^ |
100 | 99 | mpteq1d 4738 |
. . . . . 6
..^ ..^ ..^ ..^ |
101 | 97, 100 | eqtr4d 2659 |
. . . . 5
++ ..^ ..^ |
102 | 85, 89, 93, 95, 101 | offval2 6914 |
. . . 4
++ ++ ..^ ..^ ..^ |
103 | 9 | adantr 481 |
. . . . . . . . 9
..^ |
104 | 103 | oveq2d 6666 |
. . . . . . . 8
..^ ..^ ..^ |
105 | 104 | eleq2d 2687 |
. . . . . . 7
..^ ..^
..^ |
106 | 103 | oveq2d 6666 |
. . . . . . . 8
..^ |
107 | 106 | fveq2d 6195 |
. . . . . . 7
..^ |
108 | 105, 107 | ifbieq2d 4111 |
. . . . . 6
..^ ..^ ..^ |
109 | 108 | oveq2d 6666 |
. . . . 5
..^ ..^ ..^ ..^ ..^ |
110 | 109 | mpteq2dva 4744 |
. . . 4
..^ ..^ ..^ ..^ ..^ ..^ |
111 | 102, 110 | eqtr4d 2659 |
. . 3
++ ++ ..^ ..^ ..^ |
112 | | ovif12 6739 |
. . . 4
..^ ..^ ..^ |
113 | 112 | mpteq2i 4741 |
. . 3
..^ ..^ ..^ ..^ ..^ |
114 | 111, 113 | syl6eq 2672 |
. 2
++ ++ ..^ ..^ |
115 | 68, 84, 114 | 3eqtr4rd 2667 |
1
++ ++ ++ |