Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
..^ ..^ |
2 | | eqid 2622 |
. . . . 5
..^ ..^ |
3 | | ovexd 6680 |
. . . . 5
..^ |
4 | | nnex 11026 |
. . . . . . 7
|
5 | 4 | a1i 11 |
. . . . . 6
|
6 | | reprpmtf1o.a |
. . . . . 6
|
7 | 5, 6 | ssexd 4805 |
. . . . 5
|
8 | | reprpmtf1o.x |
. . . . . 6
..^ |
9 | | reprpmtf1o.s |
. . . . . . 7
|
10 | | lbfzo0 12507 |
. . . . . . 7
..^
|
11 | 9, 10 | sylibr 224 |
. . . . . 6
..^ |
12 | | reprpmtf1o.t |
. . . . . 6
..^ pmTrsp..^ |
13 | 3, 8, 11, 12 | pmtridf1o 29856 |
. . . . 5
..^..^ |
14 | 1, 1, 2, 3, 3, 7, 13 | fmptco1f1o 29434 |
. . . 4
..^ ..^ ..^ |
15 | | f1of1 6136 |
. . . 4
..^ ..^ ..^ ..^ ..^ ..^ |
16 | 14, 15 | syl 17 |
. . 3
..^ ..^ ..^ |
17 | | ssrab2 3687 |
. . . . . 6
..^ ..^
..^ |
18 | | reprpmtf1o.p |
. . . . . . . . . 10
repr |
19 | 18 | ssrab3 3688 |
. . . . . . . . 9
repr |
20 | 19 | a1i 11 |
. . . . . . . 8
repr |
21 | | reprpmtf1o.m |
. . . . . . . . 9
|
22 | 9 | nnnn0d 11351 |
. . . . . . . . 9
|
23 | 6, 21, 22 | reprval 30688 |
. . . . . . . 8
repr ..^ ..^ |
24 | 20, 23 | sseqtrd 3641 |
. . . . . . 7
..^ ..^ |
25 | 24 | sselda 3603 |
. . . . . 6
..^ ..^ |
26 | 17, 25 | sseldi 3601 |
. . . . 5
..^ |
27 | 26 | ex 450 |
. . . 4
..^ |
28 | 27 | ssrdv 3609 |
. . 3
..^ |
29 | | f1ores 6151 |
. . 3
..^ ..^ ..^ ..^
..^ ..^ |
30 | 16, 28, 29 | syl2anc 693 |
. 2
..^ ..^ |
31 | | resmpt 5449 |
. . . . 5
..^ ..^ |
32 | 28, 31 | syl 17 |
. . . 4
..^ |
33 | | reprpmtf1o.f |
. . . 4
|
34 | 32, 33 | syl6eqr 2674 |
. . 3
..^ |
35 | | eqidd 2623 |
. . 3
|
36 | | vex 3203 |
. . . . . . . . 9
|
37 | 36 | a1i 11 |
. . . . . . . 8
|
38 | 2, 37, 28 | elimampt 29438 |
. . . . . . 7
..^
|
39 | | simpr 477 |
. . . . . . . . . . . . 13
|
40 | | f1of 6137 |
. . . . . . . . . . . . . . . . 17
..^ ..^ ..^ ..^ ..^ ..^ |
41 | 14, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ ..^ ..^ |
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
..^ ..^ ..^ |
43 | 2 | fmpt 6381 |
. . . . . . . . . . . . . . 15
..^ ..^
..^ ..^ ..^ |
44 | 42, 43 | sylibr 224 |
. . . . . . . . . . . . . 14
..^ ..^ |
45 | 26 | adantr 481 |
. . . . . . . . . . . . . 14
..^ |
46 | | rspa 2930 |
. . . . . . . . . . . . . 14
..^ ..^ ..^ ..^ |
47 | 44, 45, 46 | syl2anc 693 |
. . . . . . . . . . . . 13
..^ |
48 | 39, 47 | eqeltrd 2701 |
. . . . . . . . . . . 12
..^ |
49 | 39 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^
|
50 | 49 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
..^
|
51 | | f1ofun 6139 |
. . . . . . . . . . . . . . . . . . 19
..^..^
|
52 | 13, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
..^
|
54 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
55 | | f1odm 6141 |
. . . . . . . . . . . . . . . . . . . 20
..^..^
..^ |
56 | 13, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^ |
57 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
58 | 54, 57 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . 17
..^
|
59 | | fvco 6274 |
. . . . . . . . . . . . . . . . 17
|
60 | 53, 58, 59 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^
|
61 | 60 | adantlr 751 |
. . . . . . . . . . . . . . 15
..^
|
62 | 50, 61 | eqtrd 2656 |
. . . . . . . . . . . . . 14
..^
|
63 | 62 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
..^ ..^ |
64 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
65 | | fzofi 12773 |
. . . . . . . . . . . . . . . 16
..^ |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . 15
..^ |
67 | 13 | adantr 481 |
. . . . . . . . . . . . . . 15
..^..^ |
68 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
..^
|
69 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
..^
|
70 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 20 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
repr |
74 | 70, 71, 72, 73 | reprf 30690 |
. . . . . . . . . . . . . . . . . 18
..^ |
75 | 74 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
..^
|
76 | 69, 75 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
..^
|
77 | 76 | nncnd 11036 |
. . . . . . . . . . . . . . 15
..^
|
78 | 64, 66, 67, 68, 77 | fsumf1o 14454 |
. . . . . . . . . . . . . 14
..^ ..^ |
79 | 78 | adantr 481 |
. . . . . . . . . . . . 13
..^ ..^ |
80 | 70, 71, 72, 73 | reprsum 30691 |
. . . . . . . . . . . . . 14
..^ |
81 | 80 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
82 | 63, 79, 81 | 3eqtr2d 2662 |
. . . . . . . . . . . 12
..^ |
83 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
84 | 83 | sumeq2sdv 14435 |
. . . . . . . . . . . . . 14
..^ ..^ |
85 | 84 | eqeq1d 2624 |
. . . . . . . . . . . . 13
..^ ..^ |
86 | 85 | elrab 3363 |
. . . . . . . . . . . 12
..^ ..^
..^ ..^ |
87 | 48, 82, 86 | sylanbrc 698 |
. . . . . . . . . . 11
..^ ..^ |
88 | 23 | ad2antrr 762 |
. . . . . . . . . . 11
repr ..^ ..^ |
89 | 87, 88 | eleqtrrd 2704 |
. . . . . . . . . 10
repr |
90 | 39 | fveq1d 6193 |
. . . . . . . . . . 11
|
91 | 52 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
92 | 11, 56 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
|
93 | 92 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
94 | | fvco 6274 |
. . . . . . . . . . . . 13
|
95 | 91, 93, 94 | syl2anc 693 |
. . . . . . . . . . . 12
|
96 | 3, 8, 11, 12 | pmtridfv2 29858 |
. . . . . . . . . . . . . . 15
|
97 | 96 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
98 | 97 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
99 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
100 | 99, 18 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
repr |
101 | | rabid 3116 |
. . . . . . . . . . . . . . . 16
repr
repr |
102 | 100, 101 | sylib 208 |
. . . . . . . . . . . . . . 15
repr |
103 | 102 | simprd 479 |
. . . . . . . . . . . . . 14
|
104 | 103 | adantr 481 |
. . . . . . . . . . . . 13
|
105 | 98, 104 | eqneltrd 2720 |
. . . . . . . . . . . 12
|
106 | 95, 105 | eqneltrd 2720 |
. . . . . . . . . . 11
|
107 | 90, 106 | eqneltrd 2720 |
. . . . . . . . . 10
|
108 | 89, 107 | jca 554 |
. . . . . . . . 9
repr |
109 | 108 | r19.29an 3077 |
. . . . . . . 8
repr |
110 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
repr |
111 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
repr |
112 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
repr |
113 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
repr repr |
114 | 110, 111,
112, 113 | reprf 30690 |
. . . . . . . . . . . . . . . . 17
repr ..^ |
115 | | f1ocnv 6149 |
. . . . . . . . . . . . . . . . . . 19
..^..^ ..^..^ |
116 | | f1of 6137 |
. . . . . . . . . . . . . . . . . . 19
..^..^ ..^..^ |
117 | 13, 115, 116 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
..^..^ |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . 17
repr ..^..^ |
119 | | fco 6058 |
. . . . . . . . . . . . . . . . 17
..^ ..^..^ ..^ |
120 | 114, 118,
119 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
repr ..^ |
121 | | elmapg 7870 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
..^ |
122 | 7, 3, 121 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . . . 16
repr ..^ ..^ |
124 | 120, 123 | mpbird 247 |
. . . . . . . . . . . . . . 15
repr ..^ |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . 14
repr ..^ |
126 | | f1ofun 6139 |
. . . . . . . . . . . . . . . . . . . 20
..^..^
|
127 | 13, 115, 126 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 127 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
repr ..^
|
129 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
130 | | f1odm 6141 |
. . . . . . . . . . . . . . . . . . . . . 22
..^..^
..^ |
131 | 13, 115, 130 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
132 | 131 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
133 | 129, 132 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . 19
..^ |
134 | 133 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
repr ..^
|
135 | | fvco 6274 |
. . . . . . . . . . . . . . . . . 18
|
136 | 128, 134,
135 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
repr ..^
|
137 | 136 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
repr ..^ ..^ |
138 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
139 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . 17
repr ..^ |
140 | 13, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^..^ |
141 | 140 | adantr 481 |
. . . . . . . . . . . . . . . . 17
repr ..^..^ |
142 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
repr ..^
|
143 | 110 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
repr ..^
|
144 | 114 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
repr ..^
|
145 | 143, 144 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
repr ..^
|
146 | 145 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
repr ..^
|
147 | 138, 139,
141, 142, 146 | fsumf1o 14454 |
. . . . . . . . . . . . . . . 16
repr ..^ ..^ |
148 | 110, 111,
112, 113 | reprsum 30691 |
. . . . . . . . . . . . . . . 16
repr ..^ |
149 | 137, 147,
148 | 3eqtr2d 2662 |
. . . . . . . . . . . . . . 15
repr ..^ |
150 | 149 | adantr 481 |
. . . . . . . . . . . . . 14
repr ..^ |
151 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
152 | 151 | sumeq2sdv 14435 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
153 | 152 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
..^ ..^ |
154 | 153 | elrab 3363 |
. . . . . . . . . . . . . 14
..^ ..^
..^
..^ |
155 | 125, 150,
154 | sylanbrc 698 |
. . . . . . . . . . . . 13
repr ..^ ..^ |
156 | 23 | ad2antrr 762 |
. . . . . . . . . . . . 13
repr repr ..^
..^ |
157 | 155, 156 | eleqtrrd 2704 |
. . . . . . . . . . . 12
repr repr |
158 | 127 | ad2antrr 762 |
. . . . . . . . . . . . . 14
repr |
159 | 8, 131 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
|
160 | 159 | ad2antrr 762 |
. . . . . . . . . . . . . 14
repr |
161 | | fvco 6274 |
. . . . . . . . . . . . . 14
|
162 | 158, 160,
161 | syl2anc 693 |
. . . . . . . . . . . . 13
repr |
163 | | f1ocnvfv 6534 |
. . . . . . . . . . . . . . . . . 18
..^..^ ..^
|
164 | 163 | imp 445 |
. . . . . . . . . . . . . . . . 17
..^..^ ..^ |
165 | 13, 11, 96, 164 | syl21anc 1325 |
. . . . . . . . . . . . . . . 16
|
166 | 165 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
repr |
167 | 166 | fveq2d 6195 |
. . . . . . . . . . . . . 14
repr |
168 | | simpr 477 |
. . . . . . . . . . . . . 14
repr |
169 | 167, 168 | eqneltrd 2720 |
. . . . . . . . . . . . 13
repr |
170 | 162, 169 | eqneltrd 2720 |
. . . . . . . . . . . 12
repr |
171 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
172 | 171 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
173 | 172 | notbid 308 |
. . . . . . . . . . . . 13
|
174 | 173 | elrab 3363 |
. . . . . . . . . . . 12
repr
repr |
175 | 157, 170,
174 | sylanbrc 698 |
. . . . . . . . . . 11
repr repr |
176 | 175, 18 | syl6eleqr 2712 |
. . . . . . . . . 10
repr |
177 | 176 | anasss 679 |
. . . . . . . . 9
repr |
178 | | simpr 477 |
. . . . . . . . . . 11
repr |
179 | 178 | coeq1d 5283 |
. . . . . . . . . 10
repr |
180 | 179 | eqeq2d 2632 |
. . . . . . . . 9
repr |
181 | | f1ococnv1 6165 |
. . . . . . . . . . . . . 14
..^..^
..^ |
182 | 13, 181 | syl 17 |
. . . . . . . . . . . . 13
..^ |
183 | 182 | adantr 481 |
. . . . . . . . . . . 12
repr
..^ |
184 | 183 | coeq2d 5284 |
. . . . . . . . . . 11
repr
..^ |
185 | 114 | adantrr 753 |
. . . . . . . . . . . 12
repr ..^ |
186 | | fcoi1 6078 |
. . . . . . . . . . . 12
..^ ..^ |
187 | 185, 186 | syl 17 |
. . . . . . . . . . 11
repr ..^ |
188 | 184, 187 | eqtr2d 2657 |
. . . . . . . . . 10
repr |
189 | | coass 5654 |
. . . . . . . . . 10
|
190 | 188, 189 | syl6eqr 2674 |
. . . . . . . . 9
repr |
191 | 177, 180,
190 | rspcedvd 3317 |
. . . . . . . 8
repr
|
192 | 109, 191 | impbida 877 |
. . . . . . 7
repr |
193 | 38, 192 | bitrd 268 |
. . . . . 6
..^ repr |
194 | | fveq1 6190 |
. . . . . . . . 9
|
195 | 194 | eleq1d 2686 |
. . . . . . . 8
|
196 | 195 | notbid 308 |
. . . . . . 7
|
197 | 196 | elrab 3363 |
. . . . . 6
repr
repr |
198 | 193, 197 | syl6bbr 278 |
. . . . 5
..^ repr |
199 | 198 | eqrdv 2620 |
. . . 4
..^ repr |
200 | | reprpmtf1o.o |
. . . 4
repr |
201 | 199, 200 | syl6eqr 2674 |
. . 3
..^ |
202 | 34, 35, 201 | f1oeq123d 6133 |
. 2
..^ ..^ |
203 | 30, 202 | mpbid 222 |
1
|