Metamath Proof Explorer


Theorem poimirlem26

Description: Lemma for poimir showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) of Kulpa p. 548. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φN
poimirlem28.1 p=1sts+f2nds1j×12ndsj+1N×0B=C
poimirlem28.2 φp:1N0KB0N
Assertion poimirlem26 φ2t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C

Proof

Step Hyp Ref Expression
1 poimir.0 φN
2 poimirlem28.1 p=1sts+f2nds1j×12ndsj+1N×0B=C
3 poimirlem28.2 φp:1N0KB0N
4 fzofi 0..^KFin
5 fzfi 1NFin
6 mapfi 0..^KFin1NFin0..^K1NFin
7 4 5 6 mp2an 0..^K1NFin
8 mapfi 1NFin1NFin1N1NFin
9 5 5 8 mp2an 1N1NFin
10 f1of f:1N1-1 onto1Nf:1N1N
11 10 ss2abi f|f:1N1-1 onto1Nf|f:1N1N
12 ovex 1NV
13 12 12 mapval 1N1N=f|f:1N1N
14 11 13 sseqtrri f|f:1N1-1 onto1N1N1N
15 ssfi 1N1NFinf|f:1N1-1 onto1N1N1Nf|f:1N1-1 onto1NFin
16 9 14 15 mp2an f|f:1N1-1 onto1NFin
17 7 16 pm3.2i 0..^K1NFinf|f:1N1-1 onto1NFin
18 xpfi 0..^K1NFinf|f:1N1-1 onto1NFin0..^K1N×f|f:1N1-1 onto1NFin
19 17 18 mp1i φ0..^K1N×f|f:1N1-1 onto1NFin
20 2z 2
21 20 a1i φ2
22 snfi xFin
23 fzfi 0NFin
24 rabfi 0NFiny0N|i0N1j0Nyi=x/sCj0NNx/sCFin
25 23 24 ax-mp y0N|i0N1j0Nyi=x/sCj0NNx/sCFin
26 xpfi xFiny0N|i0N1j0Nyi=x/sCj0NNx/sCFinx×y0N|i0N1j0Nyi=x/sCj0NNx/sCFin
27 22 25 26 mp2an x×y0N|i0N1j0Nyi=x/sCj0NNx/sCFin
28 hashcl x×y0N|i0N1j0Nyi=x/sCj0NNx/sCFinx×y0N|i0N1j0Nyi=x/sCj0NNx/sC0
29 27 28 ax-mp x×y0N|i0N1j0Nyi=x/sCj0NNx/sC0
30 29 nn0zi x×y0N|i0N1j0Nyi=x/sCj0NNx/sC
31 30 a1i φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
32 1 ad2antrr φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCN
33 nfv jp=1stt+f2ndt1k×12ndtk+1N×0
34 nfcsb1v _jk/jt/sC
35 34 nfeq2 jB=k/jt/sC
36 33 35 nfim jp=1stt+f2ndt1k×12ndtk+1N×0B=k/jt/sC
37 oveq2 j=k1j=1k
38 37 imaeq2d j=k2ndt1j=2ndt1k
39 38 xpeq1d j=k2ndt1j×1=2ndt1k×1
40 oveq1 j=kj+1=k+1
41 40 oveq1d j=kj+1N=k+1N
42 41 imaeq2d j=k2ndtj+1N=2ndtk+1N
43 42 xpeq1d j=k2ndtj+1N×0=2ndtk+1N×0
44 39 43 uneq12d j=k2ndt1j×12ndtj+1N×0=2ndt1k×12ndtk+1N×0
45 44 oveq2d j=k1stt+f2ndt1j×12ndtj+1N×0=1stt+f2ndt1k×12ndtk+1N×0
46 45 eqeq2d j=kp=1stt+f2ndt1j×12ndtj+1N×0p=1stt+f2ndt1k×12ndtk+1N×0
47 csbeq1a j=kt/sC=k/jt/sC
48 47 eqeq2d j=kB=t/sCB=k/jt/sC
49 46 48 imbi12d j=kp=1stt+f2ndt1j×12ndtj+1N×0B=t/sCp=1stt+f2ndt1k×12ndtk+1N×0B=k/jt/sC
50 nfv sp=1stt+f2ndt1j×12ndtj+1N×0
51 nfcsb1v _st/sC
52 51 nfeq2 sB=t/sC
53 50 52 nfim sp=1stt+f2ndt1j×12ndtj+1N×0B=t/sC
54 fveq2 s=t1sts=1stt
55 fveq2 s=t2nds=2ndt
56 55 imaeq1d s=t2nds1j=2ndt1j
57 56 xpeq1d s=t2nds1j×1=2ndt1j×1
58 55 imaeq1d s=t2ndsj+1N=2ndtj+1N
59 58 xpeq1d s=t2ndsj+1N×0=2ndtj+1N×0
60 57 59 uneq12d s=t2nds1j×12ndsj+1N×0=2ndt1j×12ndtj+1N×0
61 54 60 oveq12d s=t1sts+f2nds1j×12ndsj+1N×0=1stt+f2ndt1j×12ndtj+1N×0
62 61 eqeq2d s=tp=1sts+f2nds1j×12ndsj+1N×0p=1stt+f2ndt1j×12ndtj+1N×0
63 csbeq1a s=tC=t/sC
64 63 eqeq2d s=tB=CB=t/sC
65 62 64 imbi12d s=tp=1sts+f2nds1j×12ndsj+1N×0B=Cp=1stt+f2ndt1j×12ndtj+1N×0B=t/sC
66 53 65 2 chvarfv p=1stt+f2ndt1j×12ndtj+1N×0B=t/sC
67 36 49 66 chvarfv p=1stt+f2ndt1k×12ndtk+1N×0B=k/jt/sC
68 3 ad4ant14 φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCp:1N0KB0N
69 xp1st x0..^K1N×f|f:1N1-1 onto1N1stx0..^K1N
70 elmapi 1stx0..^K1N1stx:1N0..^K
71 69 70 syl x0..^K1N×f|f:1N1-1 onto1N1stx:1N0..^K
72 71 ad2antlr φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sC1stx:1N0..^K
73 xp2nd x0..^K1N×f|f:1N1-1 onto1N2ndxf|f:1N1-1 onto1N
74 fvex 2ndxV
75 f1oeq1 f=2ndxf:1N1-1 onto1N2ndx:1N1-1 onto1N
76 74 75 elab 2ndxf|f:1N1-1 onto1N2ndx:1N1-1 onto1N
77 73 76 sylib x0..^K1N×f|f:1N1-1 onto1N2ndx:1N1-1 onto1N
78 77 ad2antlr φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sC2ndx:1N1-1 onto1N
79 nfcv _jN
80 nfcv _jx
81 80 34 nfcsbw _jx/tk/jt/sC
82 79 81 nfne jNx/tk/jt/sC
83 nfcv _tC
84 83 51 63 cbvcsbw x/sC=x/tt/sC
85 47 csbeq2dv j=kx/tt/sC=x/tk/jt/sC
86 84 85 eqtrid j=kx/sC=x/tk/jt/sC
87 86 neeq2d j=kNx/sCNx/tk/jt/sC
88 82 87 rspc k0Nj0NNx/sCNx/tk/jt/sC
89 88 impcom j0NNx/sCk0NNx/tk/jt/sC
90 89 adantll φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCk0NNx/tk/jt/sC
91 1st2nd2 x0..^K1N×f|f:1N1-1 onto1Nx=1stx2ndx
92 91 csbeq1d x0..^K1N×f|f:1N1-1 onto1Nx/tk/jt/sC=1stx2ndx/tk/jt/sC
93 92 ad3antlr φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCk0Nx/tk/jt/sC=1stx2ndx/tk/jt/sC
94 90 93 neeqtrd φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCk0NN1stx2ndx/tk/jt/sC
95 32 67 68 72 78 94 poimirlem25 φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sC2y0N|i0N1k0Nyi=1stx2ndx/tk/jt/sC
96 nfv ki=x/sC
97 81 nfeq2 ji=x/tk/jt/sC
98 86 eqeq2d j=ki=x/sCi=x/tk/jt/sC
99 96 97 98 cbvrexw j0Nyi=x/sCk0Nyi=x/tk/jt/sC
100 92 eqeq2d x0..^K1N×f|f:1N1-1 onto1Ni=x/tk/jt/sCi=1stx2ndx/tk/jt/sC
101 100 rexbidv x0..^K1N×f|f:1N1-1 onto1Nk0Nyi=x/tk/jt/sCk0Nyi=1stx2ndx/tk/jt/sC
102 99 101 bitr2id x0..^K1N×f|f:1N1-1 onto1Nk0Nyi=1stx2ndx/tk/jt/sCj0Nyi=x/sC
103 102 ralbidv x0..^K1N×f|f:1N1-1 onto1Ni0N1k0Nyi=1stx2ndx/tk/jt/sCi0N1j0Nyi=x/sC
104 iba j0NNx/sCi0N1j0Nyi=x/sCi0N1j0Nyi=x/sCj0NNx/sC
105 103 104 sylan9bb x0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCi0N1k0Nyi=1stx2ndx/tk/jt/sCi0N1j0Nyi=x/sCj0NNx/sC
106 105 rabbidv x0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCy0N|i0N1k0Nyi=1stx2ndx/tk/jt/sC=y0N|i0N1j0Nyi=x/sCj0NNx/sC
107 106 fveq2d x0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCy0N|i0N1k0Nyi=1stx2ndx/tk/jt/sC=y0N|i0N1j0Nyi=x/sCj0NNx/sC
108 107 adantll φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sCy0N|i0N1k0Nyi=1stx2ndx/tk/jt/sC=y0N|i0N1j0Nyi=x/sCj0NNx/sC
109 95 108 breqtrd φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sC2y0N|i0N1j0Nyi=x/sCj0NNx/sC
110 109 ex φx0..^K1N×f|f:1N1-1 onto1Nj0NNx/sC2y0N|i0N1j0Nyi=x/sCj0NNx/sC
111 dvds0 220
112 20 111 ax-mp 20
113 hash0 =0
114 112 113 breqtrri 2
115 simpr i0N1j0Nyi=x/sCj0NNx/sCj0NNx/sC
116 115 con3i ¬j0NNx/sC¬i0N1j0Nyi=x/sCj0NNx/sC
117 116 ralrimivw ¬j0NNx/sCy0N¬i0N1j0Nyi=x/sCj0NNx/sC
118 rabeq0 y0N|i0N1j0Nyi=x/sCj0NNx/sC=y0N¬i0N1j0Nyi=x/sCj0NNx/sC
119 117 118 sylibr ¬j0NNx/sCy0N|i0N1j0Nyi=x/sCj0NNx/sC=
120 119 fveq2d ¬j0NNx/sCy0N|i0N1j0Nyi=x/sCj0NNx/sC=
121 114 120 breqtrrid ¬j0NNx/sC2y0N|i0N1j0Nyi=x/sCj0NNx/sC
122 110 121 pm2.61d1 φx0..^K1N×f|f:1N1-1 onto1N2y0N|i0N1j0Nyi=x/sCj0NNx/sC
123 hashxp xFiny0N|i0N1j0Nyi=x/sCj0NNx/sCFinx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=xy0N|i0N1j0Nyi=x/sCj0NNx/sC
124 22 25 123 mp2an x×y0N|i0N1j0Nyi=x/sCj0NNx/sC=xy0N|i0N1j0Nyi=x/sCj0NNx/sC
125 vex xV
126 hashsng xVx=1
127 125 126 ax-mp x=1
128 127 oveq1i xy0N|i0N1j0Nyi=x/sCj0NNx/sC=1y0N|i0N1j0Nyi=x/sCj0NNx/sC
129 hashcl y0N|i0N1j0Nyi=x/sCj0NNx/sCFiny0N|i0N1j0Nyi=x/sCj0NNx/sC0
130 25 129 ax-mp y0N|i0N1j0Nyi=x/sCj0NNx/sC0
131 130 nn0cni y0N|i0N1j0Nyi=x/sCj0NNx/sC
132 131 mullidi 1y0N|i0N1j0Nyi=x/sCj0NNx/sC=y0N|i0N1j0Nyi=x/sCj0NNx/sC
133 124 128 132 3eqtri x×y0N|i0N1j0Nyi=x/sCj0NNx/sC=y0N|i0N1j0Nyi=x/sCj0NNx/sC
134 122 133 breqtrrdi φx0..^K1N×f|f:1N1-1 onto1N2x×y0N|i0N1j0Nyi=x/sCj0NNx/sC
135 19 21 31 134 fsumdvds φ2x0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
136 7 16 18 mp2an 0..^K1N×f|f:1N1-1 onto1NFin
137 xpfi 0..^K1N×f|f:1N1-1 onto1NFin0NFin0..^K1N×f|f:1N1-1 onto1N×0NFin
138 136 23 137 mp2an 0..^K1N×f|f:1N1-1 onto1N×0NFin
139 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFin
140 138 139 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFin
141 1 nncnd φN
142 npcan1 NN-1+1=N
143 141 142 syl φN-1+1=N
144 nnm1nn0 NN10
145 1 144 syl φN10
146 145 nn0zd φN1
147 uzid N1N1N1
148 peano2uz N1N1N-1+1N1
149 146 147 148 3syl φN-1+1N1
150 143 149 eqeltrrd φNN1
151 fzss2 NN10N10N
152 ssralv 0N10Ni0Nj0Ni=1stt/sCi0N1j0Ni=1stt/sC
153 150 151 152 3syl φi0Nj0Ni=1stt/sCi0N1j0Ni=1stt/sC
154 153 adantr φN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCi0N1j0Ni=1stt/sC
155 raldifb j0Nj2ndt¬i=1stt/sCj0N2ndt¬i=1stt/sC
156 nfv jφ
157 nfcsb1v _j2ndt/j1stt/sC
158 157 nfeq2 jN=2ndt/j1stt/sC
159 156 158 nfan jφN=2ndt/j1stt/sC
160 nfv ji0N1
161 159 160 nfan jφN=2ndt/j1stt/sCi0N1
162 nnel ¬j2ndtj2ndt
163 velsn j2ndtj=2ndt
164 162 163 bitri ¬j2ndtj=2ndt
165 csbeq1a j=2ndt1stt/sC=2ndt/j1stt/sC
166 165 eqeq2d j=2ndtN=1stt/sCN=2ndt/j1stt/sC
167 166 biimparc N=2ndt/j1stt/sCj=2ndtN=1stt/sC
168 1 nnred φN
169 168 ltm1d φN1<N
170 145 nn0red φN1
171 170 168 ltnled φN1<N¬NN1
172 169 171 mpbid φ¬NN1
173 elfzle2 N0N1NN1
174 172 173 nsyl φ¬N0N1
175 eleq1 i=Ni0N1N0N1
176 175 notbid i=N¬i0N1¬N0N1
177 174 176 syl5ibrcom φi=N¬i0N1
178 177 con2d φi0N1¬i=N
179 178 imp φi0N1¬i=N
180 eqeq2 N=1stt/sCi=Ni=1stt/sC
181 180 notbid N=1stt/sC¬i=N¬i=1stt/sC
182 179 181 syl5ibcom φi0N1N=1stt/sC¬i=1stt/sC
183 167 182 syl5 φi0N1N=2ndt/j1stt/sCj=2ndt¬i=1stt/sC
184 183 expdimp φi0N1N=2ndt/j1stt/sCj=2ndt¬i=1stt/sC
185 184 an32s φN=2ndt/j1stt/sCi0N1j=2ndt¬i=1stt/sC
186 164 185 biimtrid φN=2ndt/j1stt/sCi0N1¬j2ndt¬i=1stt/sC
187 idd φN=2ndt/j1stt/sCi0N1¬i=1stt/sC¬i=1stt/sC
188 186 187 jad φN=2ndt/j1stt/sCi0N1j2ndt¬i=1stt/sC¬i=1stt/sC
189 188 adantr φN=2ndt/j1stt/sCi0N1j0Nj2ndt¬i=1stt/sC¬i=1stt/sC
190 161 189 ralimdaa φN=2ndt/j1stt/sCi0N1j0Nj2ndt¬i=1stt/sCj0N¬i=1stt/sC
191 155 190 biimtrrid φN=2ndt/j1stt/sCi0N1j0N2ndt¬i=1stt/sCj0N¬i=1stt/sC
192 191 con3d φN=2ndt/j1stt/sCi0N1¬j0N¬i=1stt/sC¬j0N2ndt¬i=1stt/sC
193 dfrex2 j0Ni=1stt/sC¬j0N¬i=1stt/sC
194 dfrex2 j0N2ndti=1stt/sC¬j0N2ndt¬i=1stt/sC
195 192 193 194 3imtr4g φN=2ndt/j1stt/sCi0N1j0Ni=1stt/sCj0N2ndti=1stt/sC
196 195 ralimdva φN=2ndt/j1stt/sCi0N1j0Ni=1stt/sCi0N1j0N2ndti=1stt/sC
197 154 196 syld φN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCi0N1j0N2ndti=1stt/sC
198 197 expimpd φN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCi0N1j0N2ndti=1stt/sC
199 198 adantr φt0..^K1N×f|f:1N1-1 onto1N×0NN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCi0N1j0N2ndti=1stt/sC
200 199 ss2rabdv φt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC
201 hashssdif t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFint0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
202 140 200 201 sylancr φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
203 xp2nd t0..^K1N×f|f:1N1-1 onto1N×0N2ndt0N
204 df-ne N1stt/sC¬N=1stt/sC
205 204 ralbii j0NN1stt/sCj0N¬N=1stt/sC
206 ralnex j0N¬N=1stt/sC¬j0NN=1stt/sC
207 205 206 bitri j0NN1stt/sC¬j0NN=1stt/sC
208 1 nnnn0d φN0
209 nn0uz 0=0
210 208 209 eleqtrdi φN0
211 143 210 eqeltrd φN-1+10
212 fzsplit2 N-1+10NN10N=0N1N-1+1N
213 211 150 212 syl2anc φ0N=0N1N-1+1N
214 143 oveq1d φN-1+1N=NN
215 1 nnzd φN
216 fzsn NNN=N
217 215 216 syl φNN=N
218 214 217 eqtrd φN-1+1N=N
219 218 uneq2d φ0N1N-1+1N=0N1N
220 213 219 eqtrd φ0N=0N1N
221 220 raleqdv φi0Nj0Ni=1stt/sCi0N1Nj0Ni=1stt/sC
222 ralunb i0N1Nj0Ni=1stt/sCi0N1j0Ni=1stt/sCiNj0Ni=1stt/sC
223 difss 0N2ndt0N
224 ssrexv 0N2ndt0Nj0N2ndti=1stt/sCj0Ni=1stt/sC
225 223 224 ax-mp j0N2ndti=1stt/sCj0Ni=1stt/sC
226 225 ralimi i0N1j0N2ndti=1stt/sCi0N1j0Ni=1stt/sC
227 226 biantrurd i0N1j0N2ndti=1stt/sCiNj0Ni=1stt/sCi0N1j0Ni=1stt/sCiNj0Ni=1stt/sC
228 222 227 bitr4id i0N1j0N2ndti=1stt/sCi0N1Nj0Ni=1stt/sCiNj0Ni=1stt/sC
229 221 228 sylan9bb φi0N1j0N2ndti=1stt/sCi0Nj0Ni=1stt/sCiNj0Ni=1stt/sC
230 229 adantlr φ2ndt0Ni0N1j0N2ndti=1stt/sCi0Nj0Ni=1stt/sCiNj0Ni=1stt/sC
231 nn0fz0 N0N0N
232 208 231 sylib φN0N
233 232 ad2antrr φ2ndt0Ni0N1j0N2ndti=1stt/sCN0N
234 eqeq1 i=Ni=1stt/sCN=1stt/sC
235 234 rexbidv i=Nj0Ni=1stt/sCj0NN=1stt/sC
236 235 rspcva N0Ni0Nj0Ni=1stt/sCj0NN=1stt/sC
237 nfv jφ2ndt0N
238 nfcv _j0N1
239 nfre1 jj0N2ndti=1stt/sC
240 238 239 nfralw ji0N1j0N2ndti=1stt/sC
241 237 240 nfan jφ2ndt0Ni0N1j0N2ndti=1stt/sC
242 eleq1 N=1stt/sCN0N11stt/sC0N1
243 242 notbid N=1stt/sC¬N0N1¬1stt/sC0N1
244 174 243 syl5ibcom φN=1stt/sC¬1stt/sC0N1
245 244 ad3antrrr φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sC¬1stt/sC0N1
246 eldifsn j0N2ndtj0Nj2ndt
247 diffi 0NFin0N2ndtFin
248 23 247 ax-mp 0N2ndtFin
249 ssrab2 j0N2ndt|1stt/sC0N10N2ndt
250 ssdomg 0N2ndtFinj0N2ndt|1stt/sC0N10N2ndtj0N2ndt|1stt/sC0N10N2ndt
251 248 249 250 mp2 j0N2ndt|1stt/sC0N10N2ndt
252 hashdifsn 0NFin2ndt0N0N2ndt=0N1
253 23 252 mpan 2ndt0N0N2ndt=0N1
254 1cnd φ1
255 141 254 254 addsubd φN+1-1=N-1+1
256 hashfz0 N00N=N+1
257 208 256 syl φ0N=N+1
258 257 oveq1d φ0N1=N+1-1
259 hashfz0 N100N1=N-1+1
260 145 259 syl φ0N1=N-1+1
261 255 258 260 3eqtr4d φ0N1=0N1
262 253 261 sylan9eqr φ2ndt0N0N2ndt=0N1
263 fzfi 0N1Fin
264 hashen 0N2ndtFin0N1Fin0N2ndt=0N10N2ndt0N1
265 248 263 264 mp2an 0N2ndt=0N10N2ndt0N1
266 262 265 sylib φ2ndt0N0N2ndt0N1
267 rabfi 0N2ndtFinj0N2ndt|1stt/sC0N1Fin
268 248 267 ax-mp j0N2ndt|1stt/sC0N1Fin
269 eleq1 i=1stt/sCi0N11stt/sC0N1
270 269 biimpac i0N1i=1stt/sC1stt/sC0N1
271 rabid jj0N2ndt|1stt/sC0N1j0N2ndt1stt/sC0N1
272 271 simplbi2com 1stt/sC0N1j0N2ndtjj0N2ndt|1stt/sC0N1
273 270 272 syl i0N1i=1stt/sCj0N2ndtjj0N2ndt|1stt/sC0N1
274 273 impancom i0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1
275 274 ancrd i0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1i=1stt/sC
276 275 expimpd i0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1i=1stt/sC
277 276 reximdv2 i0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1i=1stt/sC
278 271 simplbi jj0N2ndt|1stt/sC0N1j0N2ndt
279 274 pm4.71rd i0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1i=1stt/sC
280 df-mpt kj0N2ndt|1stt/sC0N1k/j1stt/sC=ki|kj0N2ndt|1stt/sC0N1i=k/j1stt/sC
281 nfv kjj0N2ndt|1stt/sC0N1i=1stt/sC
282 nfrab1 _jj0N2ndt|1stt/sC0N1
283 282 nfcri jkj0N2ndt|1stt/sC0N1
284 nfcsb1v _jk/j1stt/sC
285 284 nfeq2 ji=k/j1stt/sC
286 283 285 nfan jkj0N2ndt|1stt/sC0N1i=k/j1stt/sC
287 eleq1 j=kjj0N2ndt|1stt/sC0N1kj0N2ndt|1stt/sC0N1
288 csbeq1a j=k1stt/sC=k/j1stt/sC
289 288 eqeq2d j=ki=1stt/sCi=k/j1stt/sC
290 287 289 anbi12d j=kjj0N2ndt|1stt/sC0N1i=1stt/sCkj0N2ndt|1stt/sC0N1i=k/j1stt/sC
291 281 286 290 cbvopab1 ji|jj0N2ndt|1stt/sC0N1i=1stt/sC=ki|kj0N2ndt|1stt/sC0N1i=k/j1stt/sC
292 280 291 eqtr4i kj0N2ndt|1stt/sC0N1k/j1stt/sC=ji|jj0N2ndt|1stt/sC0N1i=1stt/sC
293 292 breqi jkj0N2ndt|1stt/sC0N1k/j1stt/sCijji|jj0N2ndt|1stt/sC0N1i=1stt/sCi
294 df-br jji|jj0N2ndt|1stt/sC0N1i=1stt/sCijiji|jj0N2ndt|1stt/sC0N1i=1stt/sC
295 opabidw jiji|jj0N2ndt|1stt/sC0N1i=1stt/sCjj0N2ndt|1stt/sC0N1i=1stt/sC
296 293 294 295 3bitri jkj0N2ndt|1stt/sC0N1k/j1stt/sCijj0N2ndt|1stt/sC0N1i=1stt/sC
297 279 296 bitr4di i0N1j0N2ndti=1stt/sCjkj0N2ndt|1stt/sC0N1k/j1stt/sCi
298 278 297 sylan2 i0N1jj0N2ndt|1stt/sC0N1i=1stt/sCjkj0N2ndt|1stt/sC0N1k/j1stt/sCi
299 298 rexbidva i0N1jj0N2ndt|1stt/sC0N1i=1stt/sCjj0N2ndt|1stt/sC0N1jkj0N2ndt|1stt/sC0N1k/j1stt/sCi
300 nfcv _pj0N2ndt|1stt/sC0N1
301 nfv pjkj0N2ndt|1stt/sC0N1k/j1stt/sCi
302 nfcv _jp
303 282 284 nfmpt _jkj0N2ndt|1stt/sC0N1k/j1stt/sC
304 nfcv _ji
305 302 303 304 nfbr jpkj0N2ndt|1stt/sC0N1k/j1stt/sCi
306 breq1 j=pjkj0N2ndt|1stt/sC0N1k/j1stt/sCipkj0N2ndt|1stt/sC0N1k/j1stt/sCi
307 282 300 301 305 306 cbvrexfw jj0N2ndt|1stt/sC0N1jkj0N2ndt|1stt/sC0N1k/j1stt/sCipj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
308 299 307 bitrdi i0N1jj0N2ndt|1stt/sC0N1i=1stt/sCpj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
309 277 308 sylibd i0N1j0N2ndti=1stt/sCpj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
310 309 ralimia i0N1j0N2ndti=1stt/sCi0N1pj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
311 eqid kj0N2ndt|1stt/sC0N1k/j1stt/sC=kj0N2ndt|1stt/sC0N1k/j1stt/sC
312 nfcv _jk
313 nfcv _j0N2ndt
314 284 nfel1 jk/j1stt/sC0N1
315 288 eleq1d j=k1stt/sC0N1k/j1stt/sC0N1
316 312 313 314 315 elrabf kj0N2ndt|1stt/sC0N1k0N2ndtk/j1stt/sC0N1
317 316 simprbi kj0N2ndt|1stt/sC0N1k/j1stt/sC0N1
318 311 317 fmpti kj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N10N1
319 310 318 jctil i0N1j0N2ndti=1stt/sCkj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N10N1i0N1pj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
320 dffo4 kj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N1onto0N1kj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N10N1i0N1pj0N2ndt|1stt/sC0N1pkj0N2ndt|1stt/sC0N1k/j1stt/sCi
321 319 320 sylibr i0N1j0N2ndti=1stt/sCkj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N1onto0N1
322 fodomfi j0N2ndt|1stt/sC0N1Finkj0N2ndt|1stt/sC0N1k/j1stt/sC:j0N2ndt|1stt/sC0N1onto0N10N1j0N2ndt|1stt/sC0N1
323 268 321 322 sylancr i0N1j0N2ndti=1stt/sC0N1j0N2ndt|1stt/sC0N1
324 endomtr 0N2ndt0N10N1j0N2ndt|1stt/sC0N10N2ndtj0N2ndt|1stt/sC0N1
325 266 323 324 syl2an φ2ndt0Ni0N1j0N2ndti=1stt/sC0N2ndtj0N2ndt|1stt/sC0N1
326 sbth j0N2ndt|1stt/sC0N10N2ndt0N2ndtj0N2ndt|1stt/sC0N1j0N2ndt|1stt/sC0N10N2ndt
327 251 325 326 sylancr φ2ndt0Ni0N1j0N2ndti=1stt/sCj0N2ndt|1stt/sC0N10N2ndt
328 fisseneq 0N2ndtFinj0N2ndt|1stt/sC0N10N2ndtj0N2ndt|1stt/sC0N10N2ndtj0N2ndt|1stt/sC0N1=0N2ndt
329 248 249 327 328 mp3an12i φ2ndt0Ni0N1j0N2ndti=1stt/sCj0N2ndt|1stt/sC0N1=0N2ndt
330 329 eleq2d φ2ndt0Ni0N1j0N2ndti=1stt/sCjj0N2ndt|1stt/sC0N1j0N2ndt
331 330 biimpar φ2ndt0Ni0N1j0N2ndti=1stt/sCj0N2ndtjj0N2ndt|1stt/sC0N1
332 288 equcoms k=j1stt/sC=k/j1stt/sC
333 332 eqcomd k=jk/j1stt/sC=1stt/sC
334 333 eleq1d k=jk/j1stt/sC0N11stt/sC0N1
335 334 317 vtoclga jj0N2ndt|1stt/sC0N11stt/sC0N1
336 331 335 syl φ2ndt0Ni0N1j0N2ndti=1stt/sCj0N2ndt1stt/sC0N1
337 246 336 sylan2br φ2ndt0Ni0N1j0N2ndti=1stt/sCj0Nj2ndt1stt/sC0N1
338 337 expr φ2ndt0Ni0N1j0N2ndti=1stt/sCj0Nj2ndt1stt/sC0N1
339 338 necon1bd φ2ndt0Ni0N1j0N2ndti=1stt/sCj0N¬1stt/sC0N1j=2ndt
340 245 339 syld φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCj=2ndt
341 340 imp φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCj=2ndt
342 341 165 syl φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sC1stt/sC=2ndt/j1stt/sC
343 eqtr N=1stt/sC1stt/sC=2ndt/j1stt/sCN=2ndt/j1stt/sC
344 343 ex N=1stt/sC1stt/sC=2ndt/j1stt/sCN=2ndt/j1stt/sC
345 344 adantl φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sC1stt/sC=2ndt/j1stt/sCN=2ndt/j1stt/sC
346 342 345 mpd φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCN=2ndt/j1stt/sC
347 346 exp31 φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCN=2ndt/j1stt/sC
348 241 158 347 rexlimd φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCN=2ndt/j1stt/sC
349 236 348 syl5 φ2ndt0Ni0N1j0N2ndti=1stt/sCN0Ni0Nj0Ni=1stt/sCN=2ndt/j1stt/sC
350 233 349 mpand φ2ndt0Ni0N1j0N2ndti=1stt/sCi0Nj0Ni=1stt/sCN=2ndt/j1stt/sC
351 350 pm4.71rd φ2ndt0Ni0N1j0N2ndti=1stt/sCi0Nj0Ni=1stt/sCN=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
352 235 ralsng NiNj0Ni=1stt/sCj0NN=1stt/sC
353 1 352 syl φiNj0Ni=1stt/sCj0NN=1stt/sC
354 353 ad2antrr φ2ndt0Ni0N1j0N2ndti=1stt/sCiNj0Ni=1stt/sCj0NN=1stt/sC
355 230 351 354 3bitr3rd φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN=1stt/sCN=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
356 355 notbid φ2ndt0Ni0N1j0N2ndti=1stt/sC¬j0NN=1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
357 207 356 bitrid φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
358 357 pm5.32da φ2ndt0Ni0N1j0N2ndti=1stt/sCj0NN1stt/sCi0N1j0N2ndti=1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
359 203 358 sylan2 φt0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N2ndti=1stt/sCj0NN1stt/sCi0N1j0N2ndti=1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
360 359 rabbidva φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCj0NN1stt/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
361 nfv yt=xk
362 nfv yx0..^K1N×f|f:1N1-1 onto1N
363 nfrab1 _yy0N|i0N1j0Nyi=x/sCj0NNx/sC
364 363 nfcri yky0N|i0N1j0Nyi=x/sCj0NNx/sC
365 362 364 nfan yx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sC
366 361 365 nfan yt=xkx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sC
367 nfv kt=xyx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
368 opeq2 k=yxk=xy
369 368 eqeq2d k=yt=xkt=xy
370 eleq1 k=yky0N|i0N1j0Nyi=x/sCj0NNx/sCyy0N|i0N1j0Nyi=x/sCj0NNx/sC
371 rabid yy0N|i0N1j0Nyi=x/sCj0NNx/sCy0Ni0N1j0Nyi=x/sCj0NNx/sC
372 370 371 bitrdi k=yky0N|i0N1j0Nyi=x/sCj0NNx/sCy0Ni0N1j0Nyi=x/sCj0NNx/sC
373 372 anbi2d k=yx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sCx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
374 3anass x0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sCx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
375 373 374 bitr4di k=yx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sCx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
376 369 375 anbi12d k=yt=xkx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sCt=xyx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
377 366 367 376 cbvexv1 kt=xkx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sCyt=xyx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
378 377 exbii xkt=xkx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sCxyt=xyx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
379 eliunxp tx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sCxkt=xkx0..^K1N×f|f:1N1-1 onto1Nky0N|i0N1j0Nyi=x/sCj0NNx/sC
380 elopab txy|x0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sCxyt=xyx0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
381 378 379 380 3bitr4i tx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sCtxy|x0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
382 381 eqriv x0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=xy|x0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
383 vex yV
384 125 383 op2ndd t=xy2ndt=y
385 384 sneqd t=xy2ndt=y
386 385 difeq2d t=xy0N2ndt=0Ny
387 125 383 op1std t=xy1stt=x
388 387 csbeq1d t=xy1stt/sC=x/sC
389 388 eqeq2d t=xyi=1stt/sCi=x/sC
390 386 389 rexeqbidv t=xyj0N2ndti=1stt/sCj0Nyi=x/sC
391 390 ralbidv t=xyi0N1j0N2ndti=1stt/sCi0N1j0Nyi=x/sC
392 388 neeq2d t=xyN1stt/sCNx/sC
393 392 ralbidv t=xyj0NN1stt/sCj0NNx/sC
394 391 393 anbi12d t=xyi0N1j0N2ndti=1stt/sCj0NN1stt/sCi0N1j0Nyi=x/sCj0NNx/sC
395 394 rabxp t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCj0NN1stt/sC=xy|x0..^K1N×f|f:1N1-1 onto1Ny0Ni0N1j0Nyi=x/sCj0NNx/sC
396 382 395 eqtr4i x0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCj0NN1stt/sC
397 difrab t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC¬N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
398 360 396 397 3eqtr4g φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
399 398 fveq2d φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
400 27 a1i φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sCFin
401 inxp x×y0N|i0N1j0Nyi=x/sCj0NNx/sCt×y0N|i0N1j0Nyi=t/sCj0NNt/sC=xt×y0N|i0N1j0Nyi=x/sCj0NNx/sCy0N|i0N1j0Nyi=t/sCj0NNt/sC
402 df-ne xt¬x=t
403 disjsn2 xtxt=
404 402 403 sylbir ¬x=txt=
405 404 xpeq1d ¬x=txt×y0N|i0N1j0Nyi=x/sCj0NNx/sCy0N|i0N1j0Nyi=t/sCj0NNt/sC=×y0N|i0N1j0Nyi=x/sCj0NNx/sCy0N|i0N1j0Nyi=t/sCj0NNt/sC
406 0xp ×y0N|i0N1j0Nyi=x/sCj0NNx/sCy0N|i0N1j0Nyi=t/sCj0NNt/sC=
407 405 406 eqtrdi ¬x=txt×y0N|i0N1j0Nyi=x/sCj0NNx/sCy0N|i0N1j0Nyi=t/sCj0NNt/sC=
408 401 407 eqtrid ¬x=tx×y0N|i0N1j0Nyi=x/sCj0NNx/sCt×y0N|i0N1j0Nyi=t/sCj0NNt/sC=
409 408 orri x=tx×y0N|i0N1j0Nyi=x/sCj0NNx/sCt×y0N|i0N1j0Nyi=t/sCj0NNt/sC=
410 409 rgen2w x0..^K1N×f|f:1N1-1 onto1Nt0..^K1N×f|f:1N1-1 onto1Nx=tx×y0N|i0N1j0Nyi=x/sCj0NNx/sCt×y0N|i0N1j0Nyi=t/sCj0NNt/sC=
411 sneq x=tx=t
412 csbeq1 x=tx/sC=t/sC
413 412 eqeq2d x=ti=x/sCi=t/sC
414 413 rexbidv x=tj0Nyi=x/sCj0Nyi=t/sC
415 414 ralbidv x=ti0N1j0Nyi=x/sCi0N1j0Nyi=t/sC
416 412 neeq2d x=tNx/sCNt/sC
417 416 ralbidv x=tj0NNx/sCj0NNt/sC
418 415 417 anbi12d x=ti0N1j0Nyi=x/sCj0NNx/sCi0N1j0Nyi=t/sCj0NNt/sC
419 418 rabbidv x=ty0N|i0N1j0Nyi=x/sCj0NNx/sC=y0N|i0N1j0Nyi=t/sCj0NNt/sC
420 411 419 xpeq12d x=tx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=t×y0N|i0N1j0Nyi=t/sCj0NNt/sC
421 420 disjor Disjx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sCx0..^K1N×f|f:1N1-1 onto1Nt0..^K1N×f|f:1N1-1 onto1Nx=tx×y0N|i0N1j0Nyi=x/sCj0NNx/sCt×y0N|i0N1j0Nyi=t/sCj0NNt/sC=
422 410 421 mpbir Disjx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
423 422 a1i φDisjx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
424 19 400 423 hashiun φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=x0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
425 399 424 eqtr3d φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=x0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC
426 fo1st 1st:VontoV
427 fofun 1st:VontoVFun1st
428 426 427 ax-mp Fun1st
429 ssv t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCV
430 fof 1st:VontoV1st:VV
431 426 430 ax-mp 1st:VV
432 431 fdmi dom1st=V
433 429 432 sseqtrri t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCdom1st
434 fores Fun1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCdom1st1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sConto1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
435 428 433 434 mp2an 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sConto1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
436 fveq2 t=x2ndt=2ndx
437 436 csbeq1d t=x2ndt/j1stt/sC=2ndx/j1stt/sC
438 fveq2 t=x1stt=1stx
439 438 csbeq1d t=x1stt/sC=1stx/sC
440 439 csbeq2dv t=x2ndx/j1stt/sC=2ndx/j1stx/sC
441 437 440 eqtrd t=x2ndt/j1stt/sC=2ndx/j1stx/sC
442 441 eqeq2d t=xN=2ndt/j1stt/sCN=2ndx/j1stx/sC
443 439 eqeq2d t=xi=1stt/sCi=1stx/sC
444 443 rexbidv t=xj0Ni=1stt/sCj0Ni=1stx/sC
445 444 ralbidv t=xi0Nj0Ni=1stt/sCi0Nj0Ni=1stx/sC
446 442 445 anbi12d t=xN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
447 446 rexrab xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=sx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=s
448 xp1st x0..^K1N×f|f:1N1-1 onto1N×0N1stx0..^K1N×f|f:1N1-1 onto1N
449 448 anim1i x0..^K1N×f|f:1N1-1 onto1N×0Ni0Nj0Ni=1stx/sC1stx0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=1stx/sC
450 eleq1 1stx=s1stx0..^K1N×f|f:1N1-1 onto1Ns0..^K1N×f|f:1N1-1 onto1N
451 csbeq1a s=1stxC=1stx/sC
452 451 eqcoms 1stx=sC=1stx/sC
453 452 eqcomd 1stx=s1stx/sC=C
454 453 eqeq2d 1stx=si=1stx/sCi=C
455 454 rexbidv 1stx=sj0Ni=1stx/sCj0Ni=C
456 455 ralbidv 1stx=si0Nj0Ni=1stx/sCi0Nj0Ni=C
457 450 456 anbi12d 1stx=s1stx0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=1stx/sCs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
458 449 457 syl5ibcom x0..^K1N×f|f:1N1-1 onto1N×0Ni0Nj0Ni=1stx/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
459 458 adantrl x0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
460 459 expimpd x0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
461 460 rexlimiv x0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
462 simplr φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=Cs0..^K1N×f|f:1N1-1 onto1N
463 ovex 0NV
464 463 enref 0N0N
465 phpreu 0NFin0N0Ni0Nj0Ni=Ci0N∃!j0Ni=C
466 23 464 465 mp2an i0Nj0Ni=Ci0N∃!j0Ni=C
467 466 biimpi i0Nj0Ni=Ci0N∃!j0Ni=C
468 eqeq1 i=Ni=CN=C
469 468 reubidv i=N∃!j0Ni=C∃!j0NN=C
470 469 rspcva N0Ni0N∃!j0Ni=C∃!j0NN=C
471 232 467 470 syl2an φi0Nj0Ni=C∃!j0NN=C
472 riotacl ∃!j0NN=Cιj0N|N=C0N
473 471 472 syl φi0Nj0Ni=Cιj0N|N=C0N
474 473 adantlr φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=Cιj0N|N=C0N
475 opelxpi s0..^K1N×f|f:1N1-1 onto1Nιj0N|N=C0Nsιj0N|N=C0..^K1N×f|f:1N1-1 onto1N×0N
476 462 474 475 syl2anc φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=Csιj0N|N=C0..^K1N×f|f:1N1-1 onto1N×0N
477 riotasbc ∃!j0NN=C[˙ιj0N|N=C/j]˙N=C
478 471 477 syl φi0Nj0Ni=C[˙ιj0N|N=C/j]˙N=C
479 riotaex ιj0N|N=CV
480 sbceq2g ιj0N|N=CV[˙ιj0N|N=C/j]˙N=CN=ιj0N|N=C/jC
481 479 480 ax-mp [˙ιj0N|N=C/j]˙N=CN=ιj0N|N=C/jC
482 478 481 sylib φi0Nj0Ni=CN=ιj0N|N=C/jC
483 482 expcom i0Nj0Ni=CφN=ιj0N|N=C/jC
484 483 imdistanri φi0Nj0Ni=CN=ιj0N|N=C/jCi0Nj0Ni=C
485 484 adantlr φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=CN=ιj0N|N=C/jCi0Nj0Ni=C
486 vex sV
487 486 479 op2ndd x=sιj0N|N=C2ndx=ιj0N|N=C
488 487 csbeq1d x=sιj0N|N=C2ndx/jC=ιj0N|N=C/jC
489 nfcv _js
490 nfriota1 _jιj0N|N=C
491 489 490 nfop _jsιj0N|N=C
492 491 nfeq2 jx=sιj0N|N=C
493 486 479 op1std x=sιj0N|N=C1stx=s
494 493 eqcomd x=sιj0N|N=Cs=1stx
495 494 451 syl x=sιj0N|N=CC=1stx/sC
496 492 495 csbeq2d x=sιj0N|N=C2ndx/jC=2ndx/j1stx/sC
497 488 496 eqtr3d x=sιj0N|N=Cιj0N|N=C/jC=2ndx/j1stx/sC
498 497 eqeq2d x=sιj0N|N=CN=ιj0N|N=C/jCN=2ndx/j1stx/sC
499 495 eqeq2d x=sιj0N|N=Ci=Ci=1stx/sC
500 492 499 rexbid x=sιj0N|N=Cj0Ni=Cj0Ni=1stx/sC
501 500 ralbidv x=sιj0N|N=Ci0Nj0Ni=Ci0Nj0Ni=1stx/sC
502 498 501 anbi12d x=sιj0N|N=CN=ιj0N|N=C/jCi0Nj0Ni=CN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
503 493 biantrud x=sιj0N|N=CN=2ndx/j1stx/sCi0Nj0Ni=1stx/sCN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=s
504 502 503 bitr2d x=sιj0N|N=CN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=sN=ιj0N|N=C/jCi0Nj0Ni=C
505 504 rspcev sιj0N|N=C0..^K1N×f|f:1N1-1 onto1N×0NN=ιj0N|N=C/jCi0Nj0Ni=Cx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=s
506 476 485 505 syl2anc φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=Cx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=s
507 506 expl φs0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=Cx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=s
508 461 507 impbid2 φx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
509 447 508 bitrid φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
510 509 abbidv φs|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=s=s|s0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
511 dfimafn Fun1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCdom1st1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=y|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=y
512 428 433 511 mp2an 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=y|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=y
513 nfcv _s2ndt
514 nfcsb1v _s1stt/sC
515 513 514 nfcsbw _s2ndt/j1stt/sC
516 515 nfeq2 sN=2ndt/j1stt/sC
517 nfcv _s0N
518 514 nfeq2 si=1stt/sC
519 517 518 nfrexw sj0Ni=1stt/sC
520 517 519 nfralw si0Nj0Ni=1stt/sC
521 516 520 nfan sN=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
522 nfcv _s0..^K1N×f|f:1N1-1 onto1N×0N
523 521 522 nfrabw _st0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC
524 nfv s1stx=y
525 523 524 nfrexw sxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=y
526 nfv yxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=s
527 eqeq2 y=s1stx=y1stx=s
528 527 rexbidv y=sxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=yxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=s
529 525 526 528 cbvabw y|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=y=s|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=s
530 512 529 eqtri 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s|xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=s
531 df-rab s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C=s|s0..^K1N×f|f:1N1-1 onto1Ni0Nj0Ni=C
532 510 530 531 3eqtr4g φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
533 foeq3 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sConto1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sContos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
534 532 533 syl φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sConto1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sContos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
535 435 534 mpbii φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sContos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
536 fof 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sContos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
537 535 536 syl φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
538 fvres xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stx
539 fvres yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCy=1sty
540 538 539 eqeqan12d xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCy1stx=1sty
541 540 adantl φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCy1stx=1sty
542 446 elrab xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
543 xp2nd x0..^K1N×f|f:1N1-1 onto1N×0N2ndx0N
544 543 anim1i x0..^K1N×f|f:1N1-1 onto1N×0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
545 542 544 sylbi xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
546 simpl N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCN=2ndt/j1stt/sC
547 546 a1i t0..^K1N×f|f:1N1-1 onto1N×0NN=2ndt/j1stt/sCi0Nj0Ni=1stt/sCN=2ndt/j1stt/sC
548 547 ss2rabi t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sC
549 548 sseli yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sC
550 fveq2 t=y2ndt=2ndy
551 550 csbeq1d t=y2ndt/j1stt/sC=2ndy/j1stt/sC
552 fveq2 t=y1stt=1sty
553 552 csbeq1d t=y1stt/sC=1sty/sC
554 553 csbeq2dv t=y2ndy/j1stt/sC=2ndy/j1sty/sC
555 551 554 eqtrd t=y2ndt/j1stt/sC=2ndy/j1sty/sC
556 555 eqeq2d t=yN=2ndt/j1stt/sCN=2ndy/j1sty/sC
557 556 elrab yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCy0..^K1N×f|f:1N1-1 onto1N×0NN=2ndy/j1sty/sC
558 xp2nd y0..^K1N×f|f:1N1-1 onto1N×0N2ndy0N
559 558 anim1i y0..^K1N×f|f:1N1-1 onto1N×0NN=2ndy/j1sty/sC2ndy0NN=2ndy/j1sty/sC
560 557 559 sylbi yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sC2ndy0NN=2ndy/j1sty/sC
561 549 560 syl yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC2ndy0NN=2ndy/j1sty/sC
562 545 561 anim12i xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndy0NN=2ndy/j1sty/sC
563 an4 2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC
564 563 anbi2i i0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC
565 anass 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC
566 ancom 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC
567 565 566 bitr3i 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC
568 567 anbi1i 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndy0NN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sC
569 anass i0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sC
570 568 569 bitri 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndy0NN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0NN=2ndx/j1stx/sC2ndy0NN=2ndy/j1sty/sC
571 anass i0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC
572 564 570 571 3bitr4i 2ndx0NN=2ndx/j1stx/sCi0Nj0Ni=1stx/sC2ndy0NN=2ndy/j1sty/sCi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC
573 562 572 sylib xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC
574 phpreu 0NFin0N0Ni0Nj0Ni=1stx/sCi0N∃!j0Ni=1stx/sC
575 23 464 574 mp2an i0Nj0Ni=1stx/sCi0N∃!j0Ni=1stx/sC
576 reurmo ∃!j0Ni=1stx/sC*j0Ni=1stx/sC
577 576 ralimi i0N∃!j0Ni=1stx/sCi0N*j0Ni=1stx/sC
578 575 577 sylbi i0Nj0Ni=1stx/sCi0N*j0Ni=1stx/sC
579 eqeq1 i=Ni=1stx/sCN=1stx/sC
580 579 rmobidv i=N*j0Ni=1stx/sC*j0NN=1stx/sC
581 580 rspcva N0Ni0N*j0Ni=1stx/sC*j0NN=1stx/sC
582 232 578 581 syl2an φi0Nj0Ni=1stx/sC*j0NN=1stx/sC
583 nfv kN=1stx/sC
584 583 rmo3 *j0NN=1stx/sCj0Nk0NN=1stx/sCkjN=1stx/sCj=k
585 582 584 sylib φi0Nj0Ni=1stx/sCj0Nk0NN=1stx/sCkjN=1stx/sCj=k
586 nfcsb1v _j2ndx/j1stx/sC
587 586 nfeq2 jN=2ndx/j1stx/sC
588 nfs1v jkjN=1stx/sC
589 587 588 nfan jN=2ndx/j1stx/sCkjN=1stx/sC
590 nfv j2ndx=k
591 589 590 nfim jN=2ndx/j1stx/sCkjN=1stx/sC2ndx=k
592 nfv kN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndy
593 csbeq1a j=2ndx1stx/sC=2ndx/j1stx/sC
594 593 eqeq2d j=2ndxN=1stx/sCN=2ndx/j1stx/sC
595 594 anbi1d j=2ndxN=1stx/sCkjN=1stx/sCN=2ndx/j1stx/sCkjN=1stx/sC
596 eqeq1 j=2ndxj=k2ndx=k
597 595 596 imbi12d j=2ndxN=1stx/sCkjN=1stx/sCj=kN=2ndx/j1stx/sCkjN=1stx/sC2ndx=k
598 sbsbc kjN=1stx/sC[˙k/j]˙N=1stx/sC
599 vex kV
600 sbceq2g kV[˙k/j]˙N=1stx/sCN=k/j1stx/sC
601 599 600 ax-mp [˙k/j]˙N=1stx/sCN=k/j1stx/sC
602 598 601 bitri kjN=1stx/sCN=k/j1stx/sC
603 csbeq1 k=2ndyk/j1stx/sC=2ndy/j1stx/sC
604 603 eqeq2d k=2ndyN=k/j1stx/sCN=2ndy/j1stx/sC
605 602 604 bitrid k=2ndykjN=1stx/sCN=2ndy/j1stx/sC
606 605 anbi2d k=2ndyN=2ndx/j1stx/sCkjN=1stx/sCN=2ndx/j1stx/sCN=2ndy/j1stx/sC
607 eqeq2 k=2ndy2ndx=k2ndx=2ndy
608 606 607 imbi12d k=2ndyN=2ndx/j1stx/sCkjN=1stx/sC2ndx=kN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndy
609 591 592 597 608 rspc2 2ndx0N2ndy0Nj0Nk0NN=1stx/sCkjN=1stx/sCj=kN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndy
610 585 609 syl5com φi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndy
611 610 impr φi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndy
612 csbeq1 1stx=1sty1stx/sC=1sty/sC
613 612 csbeq2dv 1stx=1sty2ndy/j1stx/sC=2ndy/j1sty/sC
614 613 eqeq2d 1stx=1styN=2ndy/j1stx/sCN=2ndy/j1sty/sC
615 614 anbi2d 1stx=1styN=2ndx/j1stx/sCN=2ndy/j1stx/sCN=2ndx/j1stx/sCN=2ndy/j1sty/sC
616 615 imbi1d 1stx=1styN=2ndx/j1stx/sCN=2ndy/j1stx/sC2ndx=2ndyN=2ndx/j1stx/sCN=2ndy/j1sty/sC2ndx=2ndy
617 611 616 syl5ibcom φi0Nj0Ni=1stx/sC2ndx0N2ndy0N1stx=1styN=2ndx/j1stx/sCN=2ndy/j1sty/sC2ndx=2ndy
618 617 com23 φi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC1stx=1sty2ndx=2ndy
619 618 impr φi0Nj0Ni=1stx/sC2ndx0N2ndy0NN=2ndx/j1stx/sCN=2ndy/j1sty/sC1stx=1sty2ndx=2ndy
620 573 619 sylan2 φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=1sty2ndx=2ndy
621 elrabi xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx0..^K1N×f|f:1N1-1 onto1N×0N
622 elrabi yt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCy0..^K1N×f|f:1N1-1 onto1N×0N
623 xpopth x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N1stx=1sty2ndx=2ndyx=y
624 623 biimpd x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N1stx=1sty2ndx=2ndyx=y
625 624 expd x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N1stx=1sty2ndx=2ndyx=y
626 621 622 625 syl2an xt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=1sty2ndx=2ndyx=y
627 626 adantl φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=1sty2ndx=2ndyx=y
628 620 627 mpdd φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stx=1styx=y
629 541 628 sylbid φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyx=y
630 629 ralrimivva φxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyx=y
631 dff13 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=Cxt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCyx=y
632 537 630 631 sylanbrc φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
633 df-f1o 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sContos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
634 632 535 633 sylanbrc φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
635 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCFin
636 138 635 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCFin
637 636 elexi t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCV
638 637 f1oen 1stt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC:t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=Ct0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
639 634 638 syl φt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
640 rabfi 0..^K1N×f|f:1N1-1 onto1NFins0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=CFin
641 136 640 ax-mp s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=CFin
642 hashen t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCFins0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=CFint0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=Ct0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
643 636 641 642 mp2an t0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=Ct0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
644 639 643 sylibr φt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=s0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
645 644 oveq2d φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|N=2ndt/j1stt/sCi0Nj0Ni=1stt/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
646 202 425 645 3eqtr3d φx0..^K1N×f|f:1N1-1 onto1Nx×y0N|i0N1j0Nyi=x/sCj0NNx/sC=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C
647 135 646 breqtrd φ2t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0Nj0Ni=C