Metamath Proof Explorer


Theorem poimirlem27

Description: Lemma for poimir showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) 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
poimirlem28.3 φn1Np:1N0Kpn=0B<n
poimirlem28.4 φn1Np:1N0Kpn=KBn1
Assertion poimirlem27 φ2t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N

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 poimirlem28.3 φn1Np:1N0Kpn=0B<n
5 poimirlem28.4 φn1Np:1N0Kpn=KBn1
6 fzfi 0KFin
7 fzfi 1NFin
8 mapfi 0KFin1NFin0K1NFin
9 6 7 8 mp2an 0K1NFin
10 fzfi 0N1Fin
11 mapfi 0K1NFin0N1Fin0K1N0N1Fin
12 9 10 11 mp2an 0K1N0N1Fin
13 12 a1i φ0K1N0N1Fin
14 2z 2
15 14 a1i φ2
16 fzofi 0..^KFin
17 mapfi 0..^KFin1NFin0..^K1NFin
18 16 7 17 mp2an 0..^K1NFin
19 mapfi 1NFin1NFin1N1NFin
20 7 7 19 mp2an 1N1NFin
21 f1of f:1N1-1 onto1Nf:1N1N
22 21 ss2abi f|f:1N1-1 onto1Nf|f:1N1N
23 ovex 1NV
24 23 23 mapval 1N1N=f|f:1N1N
25 22 24 sseqtrri f|f:1N1-1 onto1N1N1N
26 ssfi 1N1NFinf|f:1N1-1 onto1N1N1Nf|f:1N1-1 onto1NFin
27 20 25 26 mp2an f|f:1N1-1 onto1NFin
28 xpfi 0..^K1NFinf|f:1N1-1 onto1NFin0..^K1N×f|f:1N1-1 onto1NFin
29 18 27 28 mp2an 0..^K1N×f|f:1N1-1 onto1NFin
30 fzfi 0NFin
31 xpfi 0..^K1N×f|f:1N1-1 onto1NFin0NFin0..^K1N×f|f:1N1-1 onto1N×0NFin
32 29 30 31 mp2an 0..^K1N×f|f:1N1-1 onto1N×0NFin
33 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKFin
34 32 33 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKFin
35 hashcl t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKFint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK0
36 35 nn0zd t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKFint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
37 34 36 mp1i φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
38 dfrex2 t0..^K1N×f|f:1N1-1 onto1N×0N0N1ranpranxBn1Npranxpn0pranxpnK¬t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnK
39 nfv tφx0K1N0N1
40 nfcv _t2
41 nfcv _t
42 nfcv _t.
43 nfrab1 _tt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
44 42 43 nffv _tt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
45 40 41 44 nfbr t2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
46 neq0 ¬t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=sst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
47 iddvds 222
48 14 47 ax-mp 22
49 vex sV
50 hashsng sVs=1
51 49 50 ax-mp s=1
52 51 oveq2i 1+s=1+1
53 df-2 2=1+1
54 52 53 eqtr4i 1+s=2
55 48 54 breqtrri 21+s
56 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0Fin
57 diffi t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0Fint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0sFin
58 32 56 57 mp2b t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0sFin
59 snfi sFin
60 disjdifr t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=
61 hashun t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0sFinsFint0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s+s
62 58 59 60 61 mp3an t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s+s
63 difsnid st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
64 63 fveq2d st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0ss=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
65 62 64 eqtr3id st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s+s=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
66 65 adantl φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s+s=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
67 1 ad3antrrr φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0N
68 fveq2 t=u2ndt=2ndu
69 68 breq2d t=uy<2ndty<2ndu
70 69 ifbid t=uify<2ndtyy+1=ify<2nduyy+1
71 70 csbeq1d t=uify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2nduyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
72 2fveq3 t=u1st1stt=1st1stu
73 2fveq3 t=u2nd1stt=2nd1stu
74 73 imaeq1d t=u2nd1stt1j=2nd1stu1j
75 74 xpeq1d t=u2nd1stt1j×1=2nd1stu1j×1
76 73 imaeq1d t=u2nd1sttj+1N=2nd1stuj+1N
77 76 xpeq1d t=u2nd1sttj+1N×0=2nd1stuj+1N×0
78 75 77 uneq12d t=u2nd1stt1j×12nd1sttj+1N×0=2nd1stu1j×12nd1stuj+1N×0
79 72 78 oveq12d t=u1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1stu+f2nd1stu1j×12nd1stuj+1N×0
80 79 csbeq2dv t=uify<2nduyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0
81 71 80 eqtrd t=uify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0
82 81 mpteq2dv t=uy0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0
83 breq1 y=wy<2nduw<2ndu
84 id y=wy=w
85 oveq1 y=wy+1=w+1
86 83 84 85 ifbieq12d y=wify<2nduyy+1=ifw<2nduww+1
87 86 csbeq1d y=wify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0=ifw<2nduww+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0
88 oveq2 j=i1j=1i
89 88 imaeq2d j=i2nd1stu1j=2nd1stu1i
90 89 xpeq1d j=i2nd1stu1j×1=2nd1stu1i×1
91 oveq1 j=ij+1=i+1
92 91 oveq1d j=ij+1N=i+1N
93 92 imaeq2d j=i2nd1stuj+1N=2nd1stui+1N
94 93 xpeq1d j=i2nd1stuj+1N×0=2nd1stui+1N×0
95 90 94 uneq12d j=i2nd1stu1j×12nd1stuj+1N×0=2nd1stu1i×12nd1stui+1N×0
96 95 oveq2d j=i1st1stu+f2nd1stu1j×12nd1stuj+1N×0=1st1stu+f2nd1stu1i×12nd1stui+1N×0
97 96 cbvcsbv ifw<2nduww+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0=ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
98 87 97 eqtrdi y=wify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0=ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
99 98 cbvmptv y0N1ify<2nduyy+1/j1st1stu+f2nd1stu1j×12nd1stuj+1N×0=w0N1ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
100 82 99 eqtrdi t=uy0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=w0N1ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
101 100 eqeq2d t=ux=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0x=w0N1ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
102 101 cbvrabv t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=u0..^K1N×f|f:1N1-1 onto1N×0N|x=w0N1ifw<2nduww+1/i1st1stu+f2nd1stu1i×12nd1stui+1N×0
103 elmapi x0K1N0N1x:0N10K1N
104 103 ad3antlr φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0x:0N10K1N
105 simpr φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
106 simpl pranxpn0pranxpnKpranxpn0
107 106 ralimi n1Npranxpn0pranxpnKn1Npranxpn0
108 107 ad2antlr φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0n1Npranxpn0
109 fveq2 n=mpn=pm
110 109 neeq1d n=mpn0pm0
111 110 rexbidv n=mpranxpn0pranxpm0
112 fveq1 p=qpm=qm
113 112 neeq1d p=qpm0qm0
114 113 cbvrexvw pranxpm0qranxqm0
115 111 114 bitrdi n=mpranxpn0qranxqm0
116 115 rspccva n1Npranxpn0m1Nqranxqm0
117 108 116 sylan φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0m1Nqranxqm0
118 simpr pranxpn0pranxpnKpranxpnK
119 118 ralimi n1Npranxpn0pranxpnKn1NpranxpnK
120 119 ad2antlr φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0n1NpranxpnK
121 109 neeq1d n=mpnKpmK
122 121 rexbidv n=mpranxpnKpranxpmK
123 112 neeq1d p=qpmKqmK
124 123 cbvrexvw pranxpmKqranxqmK
125 122 124 bitrdi n=mpranxpnKqranxqmK
126 125 rspccva n1NpranxpnKm1NqranxqmK
127 120 126 sylan φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0m1NqranxqmK
128 67 102 104 105 117 127 poimirlem22 φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0∃!zt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zs
129 eldifsn zt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0szt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zs
130 129 eubii ∃!zzt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s∃!zzt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zs
131 58 elexi t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0sV
132 euhash1 t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0sVt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s=1∃!zzt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s
133 131 132 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s=1∃!zzt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s
134 df-reu ∃!zt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zs∃!zzt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zs
135 130 133 134 3bitr4ri ∃!zt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0zst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s=1
136 128 135 sylib φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s=1
137 136 oveq1d φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s+s=1+s
138 66 137 eqtr3d φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1+s
139 55 138 breqtrrid φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×02t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
140 139 ex φx0K1N0N1n1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×02t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
141 140 exlimdv φx0K1N0N1n1Npranxpn0pranxpnKsst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×02t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
142 46 141 biimtrid φx0K1N0N1n1Npranxpn0pranxpnK¬t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
143 dvds0 220
144 14 143 ax-mp 20
145 hash0 =0
146 144 145 breqtrri 2
147 fveq2 t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=
148 146 147 breqtrrid t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
149 142 148 pm2.61d2 φx0K1N0N1n1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
150 149 ex φx0K1N0N1n1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
151 150 adantld φx0K1N0N10N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
152 iba 0N1ranpranxBn1Npranxpn0pranxpnKx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
153 152 rabbidv 0N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
154 153 fveq2d 0N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
155 154 breq2d 0N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×02t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
156 151 155 mpbidi φx0K1N0N10N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
157 156 a1d φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N0N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
158 39 45 157 rexlimd φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N0N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
159 38 158 biimtrrid φx0K1N0N1¬t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
160 simpr x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK0N1ranpranxBn1Npranxpn0pranxpnK
161 160 con3i ¬0N1ranpranxBn1Npranxpn0pranxpnK¬x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
162 161 ralimi t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N¬x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
163 rabeq0 t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N¬x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
164 162 163 sylibr t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=
165 164 fveq2d t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=
166 146 165 breqtrrid t0..^K1N×f|f:1N1-1 onto1N×0N¬0N1ranpranxBn1Npranxpn0pranxpnK2t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
167 159 166 pm2.61d2 φx0K1N0N12t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
168 13 15 37 167 fsumdvds φ2x0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
169 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFin
170 32 169 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFin
171 simp1 i0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ni0N1j0N1i=1stt/sC
172 sneq 2ndt=N2ndt=N
173 172 difeq2d 2ndt=N0N2ndt=0NN
174 difun2 0N1NN=0N1N
175 1 nnnn0d φN0
176 nn0uz 0=0
177 175 176 eleqtrdi φN0
178 fzm1 N0n0Nn0N1n=N
179 177 178 syl φn0Nn0N1n=N
180 elun n0N1Nn0N1nN
181 velsn nNn=N
182 181 orbi2i n0N1nNn0N1n=N
183 180 182 bitri n0N1Nn0N1n=N
184 179 183 bitr4di φn0Nn0N1N
185 184 eqrdv φ0N=0N1N
186 185 difeq1d φ0NN=0N1NN
187 1 nnzd φN
188 uzid NNN
189 uznfz NN¬N0N1
190 187 188 189 3syl φ¬N0N1
191 disjsn 0N1N=¬N0N1
192 disj3 0N1N=0N1=0N1N
193 191 192 bitr3i ¬N0N10N1=0N1N
194 190 193 sylib φ0N1=0N1N
195 174 186 194 3eqtr4a φ0NN=0N1
196 173 195 sylan9eqr φ2ndt=N0N2ndt=0N1
197 196 rexeqdv φ2ndt=Nj0N2ndti=1stt/sCj0N1i=1stt/sC
198 197 biimprd φ2ndt=Nj0N1i=1stt/sCj0N2ndti=1stt/sC
199 198 ralimdv φ2ndt=Ni0N1j0N1i=1stt/sCi0N1j0N2ndti=1stt/sC
200 199 expimpd φ2ndt=Ni0N1j0N1i=1stt/sCi0N1j0N2ndti=1stt/sC
201 171 200 sylan2i φ2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1stt/sC
202 201 adantr φt0..^K1N×f|f:1N1-1 onto1N×0N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1stt/sC
203 202 ss2rabdv φt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC
204 hashssdif t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCFint0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nt0..^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|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
205 170 203 204 sylancr φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
206 1 adantr φt0..^K1N×f|f:1N1-1 onto1N×0NN
207 3 adantlr φt0..^K1N×f|f:1N1-1 onto1N×0Np:1N0KB0N
208 xp1st t0..^K1N×f|f:1N1-1 onto1N×0N1stt0..^K1N×f|f:1N1-1 onto1N
209 xp1st 1stt0..^K1N×f|f:1N1-1 onto1N1st1stt0..^K1N
210 elmapi 1st1stt0..^K1N1st1stt:1N0..^K
211 208 209 210 3syl t0..^K1N×f|f:1N1-1 onto1N×0N1st1stt:1N0..^K
212 211 adantl φt0..^K1N×f|f:1N1-1 onto1N×0N1st1stt:1N0..^K
213 xp2nd 1stt0..^K1N×f|f:1N1-1 onto1N2nd1sttf|f:1N1-1 onto1N
214 fvex 2nd1sttV
215 f1oeq1 f=2nd1sttf:1N1-1 onto1N2nd1stt:1N1-1 onto1N
216 214 215 elab 2nd1sttf|f:1N1-1 onto1N2nd1stt:1N1-1 onto1N
217 213 216 sylib 1stt0..^K1N×f|f:1N1-1 onto1N2nd1stt:1N1-1 onto1N
218 208 217 syl t0..^K1N×f|f:1N1-1 onto1N×0N2nd1stt:1N1-1 onto1N
219 218 adantl φt0..^K1N×f|f:1N1-1 onto1N×0N2nd1stt:1N1-1 onto1N
220 xp2nd t0..^K1N×f|f:1N1-1 onto1N×0N2ndt0N
221 220 adantl φt0..^K1N×f|f:1N1-1 onto1N×0N2ndt0N
222 206 2 207 212 219 221 poimirlem24 φt0..^K1N×f|f:1N1-1 onto1N×0Nx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBpranxpN0i0N1j0N2ndti=1st1stt2nd1stt/sC¬2ndt=N1st1sttN=02nd1sttN=N
223 208 adantl φt0..^K1N×f|f:1N1-1 onto1N×0N1stt0..^K1N×f|f:1N1-1 onto1N
224 1st2nd2 1stt0..^K1N×f|f:1N1-1 onto1N1stt=1st1stt2nd1stt
225 224 csbeq1d 1stt0..^K1N×f|f:1N1-1 onto1N1stt/sC=1st1stt2nd1stt/sC
226 225 eqeq2d 1stt0..^K1N×f|f:1N1-1 onto1Ni=1stt/sCi=1st1stt2nd1stt/sC
227 226 rexbidv 1stt0..^K1N×f|f:1N1-1 onto1Nj0N2ndti=1stt/sCj0N2ndti=1st1stt2nd1stt/sC
228 227 ralbidv 1stt0..^K1N×f|f:1N1-1 onto1Ni0N1j0N2ndti=1stt/sCi0N1j0N2ndti=1st1stt2nd1stt/sC
229 228 anbi1d 1stt0..^K1N×f|f:1N1-1 onto1Ni0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1st1stt2nd1stt/sC¬2ndt=N1st1sttN=02nd1sttN=N
230 223 229 syl φt0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1st1stt2nd1stt/sC¬2ndt=N1st1sttN=02nd1sttN=N
231 222 230 bitr4d φt0..^K1N×f|f:1N1-1 onto1N×0Nx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBpranxpN0i0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=N
232 103 frnd x0K1N0N1ranx0K1N
233 232 anim2i φx0K1N0N1φranx0K1N
234 dfss3 0N1ranpranxBn0N1nranpranxB
235 vex nV
236 eqid pranxB=pranxB
237 236 elrnmpt nVnranpranxBpranxn=B
238 235 237 ax-mp nranpranxBpranxn=B
239 238 ralbii n0N1nranpranxBn0N1pranxn=B
240 234 239 sylbb 0N1ranpranxBn0N1pranxn=B
241 1eluzge0 10
242 fzss1 101N10N1
243 ssralv 1N10N1n0N1pranxn=Bn1N1pranxn=B
244 241 242 243 mp2b n0N1pranxn=Bn1N1pranxn=B
245 1 nncnd φN
246 npcan1 NN-1+1=N
247 245 246 syl φN-1+1=N
248 peano2zm NN1
249 187 248 syl φN1
250 uzid N1N1N1
251 peano2uz N1N1N-1+1N1
252 249 250 251 3syl φN-1+1N1
253 247 252 eqeltrrd φNN1
254 fzss2 NN11N11N
255 253 254 syl φ1N11N
256 255 sselda φn1N1n1N
257 256 adantlr φranx0K1Nn1N1n1N
258 simplr φranx0K1Nn1Nranx0K1N
259 ssel2 ranx0K1Npranxp0K1N
260 elmapi p0K1Np:1N0K
261 259 260 syl ranx0K1Npranxp:1N0K
262 258 261 sylan φranx0K1Nn1Npranxp:1N0K
263 elfzelz n1Nn
264 263 zred n1Nn
265 264 ltnrd n1N¬n<n
266 breq1 n=Bn<nB<n
267 266 notbid n=B¬n<n¬B<n
268 265 267 syl5ibcom n1Nn=B¬B<n
269 268 necon2ad n1NB<nnB
270 269 3ad2ant1 n1Np:1N0Kpn=0B<nnB
271 270 adantl φn1Np:1N0Kpn=0B<nnB
272 4 271 mpd φn1Np:1N0Kpn=0nB
273 272 3exp2 φn1Np:1N0Kpn=0nB
274 273 imp31 φn1Np:1N0Kpn=0nB
275 274 necon2d φn1Np:1N0Kn=Bpn0
276 275 adantllr φranx0K1Nn1Np:1N0Kn=Bpn0
277 262 276 syldan φranx0K1Nn1Npranxn=Bpn0
278 277 reximdva φranx0K1Nn1Npranxn=Bpranxpn0
279 257 278 syldan φranx0K1Nn1N1pranxn=Bpranxpn0
280 279 ralimdva φranx0K1Nn1N1pranxn=Bn1N1pranxpn0
281 280 imp φranx0K1Nn1N1pranxn=Bn1N1pranxpn0
282 244 281 sylan2 φranx0K1Nn0N1pranxn=Bn1N1pranxpn0
283 282 biantrurd φranx0K1Nn0N1pranxn=BpranxpN0n1N1pranxpn0pranxpN0
284 nnuz =1
285 1 284 eleqtrdi φN1
286 fzm1 N1n1Nn1N1n=N
287 285 286 syl φn1Nn1N1n=N
288 elun n1N1Nn1N1nN
289 181 orbi2i n1N1nNn1N1n=N
290 288 289 bitri n1N1Nn1N1n=N
291 287 290 bitr4di φn1Nn1N1N
292 291 eqrdv φ1N=1N1N
293 292 raleqdv φn1Npranxpn0n1N1Npranxpn0
294 ralunb n1N1Npranxpn0n1N1pranxpn0nNpranxpn0
295 293 294 bitrdi φn1Npranxpn0n1N1pranxpn0nNpranxpn0
296 fveq2 n=Npn=pN
297 296 neeq1d n=Npn0pN0
298 297 rexbidv n=Npranxpn0pranxpN0
299 298 ralsng NnNpranxpn0pranxpN0
300 1 299 syl φnNpranxpn0pranxpN0
301 300 anbi2d φn1N1pranxpn0nNpranxpn0n1N1pranxpn0pranxpN0
302 295 301 bitrd φn1Npranxpn0n1N1pranxpn0pranxpN0
303 302 ad2antrr φranx0K1Nn0N1pranxn=Bn1Npranxpn0n1N1pranxpn0pranxpN0
304 0z 0
305 1z 1
306 fzshftral 0N11n0N1pranxn=Bm0+1N-1+1[˙m1/n]˙pranxn=B
307 304 305 306 mp3an13 N1n0N1pranxn=Bm0+1N-1+1[˙m1/n]˙pranxn=B
308 187 248 307 3syl φn0N1pranxn=Bm0+1N-1+1[˙m1/n]˙pranxn=B
309 0p1e1 0+1=1
310 309 a1i φ0+1=1
311 310 247 oveq12d φ0+1N-1+1=1N
312 311 raleqdv φm0+1N-1+1[˙m1/n]˙pranxn=Bm1N[˙m1/n]˙pranxn=B
313 308 312 bitrd φn0N1pranxn=Bm1N[˙m1/n]˙pranxn=B
314 ovex m1V
315 eqeq1 n=m1n=Bm1=B
316 315 rexbidv n=m1pranxn=Bpranxm1=B
317 314 316 sbcie [˙m1/n]˙pranxn=Bpranxm1=B
318 317 ralbii m1N[˙m1/n]˙pranxn=Bm1Npranxm1=B
319 oveq1 m=nm1=n1
320 319 eqeq1d m=nm1=Bn1=B
321 320 rexbidv m=npranxm1=Bpranxn1=B
322 321 cbvralvw m1Npranxm1=Bn1Npranxn1=B
323 318 322 bitri m1N[˙m1/n]˙pranxn=Bn1Npranxn1=B
324 313 323 bitrdi φn0N1pranxn=Bn1Npranxn1=B
325 324 biimpa φn0N1pranxn=Bn1Npranxn1=B
326 325 adantlr φranx0K1Nn0N1pranxn=Bn1Npranxn1=B
327 5 necomd φn1Np:1N0Kpn=Kn1B
328 327 3exp2 φn1Np:1N0Kpn=Kn1B
329 328 imp31 φn1Np:1N0Kpn=Kn1B
330 329 necon2d φn1Np:1N0Kn1=BpnK
331 330 adantllr φranx0K1Nn1Np:1N0Kn1=BpnK
332 262 331 syldan φranx0K1Nn1Npranxn1=BpnK
333 332 reximdva φranx0K1Nn1Npranxn1=BpranxpnK
334 333 ralimdva φranx0K1Nn1Npranxn1=Bn1NpranxpnK
335 334 imp φranx0K1Nn1Npranxn1=Bn1NpranxpnK
336 326 335 syldan φranx0K1Nn0N1pranxn=Bn1NpranxpnK
337 336 biantrud φranx0K1Nn0N1pranxn=Bn1Npranxpn0n1Npranxpn0n1NpranxpnK
338 r19.26 n1Npranxpn0pranxpnKn1Npranxpn0n1NpranxpnK
339 337 338 bitr4di φranx0K1Nn0N1pranxn=Bn1Npranxpn0n1Npranxpn0pranxpnK
340 283 303 339 3bitr2d φranx0K1Nn0N1pranxn=BpranxpN0n1Npranxpn0pranxpnK
341 233 240 340 syl2an φx0K1N0N10N1ranpranxBpranxpN0n1Npranxpn0pranxpnK
342 341 pm5.32da φx0K1N0N10N1ranpranxBpranxpN00N1ranpranxBn1Npranxpn0pranxpnK
343 342 anbi2d φx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBpranxpN0x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
344 343 rexbidva φx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBpranxpN0x0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
345 344 adantr φt0..^K1N×f|f:1N1-1 onto1N×0Nx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBpranxpN0x0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
346 195 rexeqdv φj0NNi=1stt/sCj0N1i=1stt/sC
347 346 biimpd φj0NNi=1stt/sCj0N1i=1stt/sC
348 347 ralimdv φi0N1j0NNi=1stt/sCi0N1j0N1i=1stt/sC
349 173 rexeqdv 2ndt=Nj0N2ndti=1stt/sCj0NNi=1stt/sC
350 349 ralbidv 2ndt=Ni0N1j0N2ndti=1stt/sCi0N1j0NNi=1stt/sC
351 350 imbi1d 2ndt=Ni0N1j0N2ndti=1stt/sCi0N1j0N1i=1stt/sCi0N1j0NNi=1stt/sCi0N1j0N1i=1stt/sC
352 348 351 syl5ibrcom φ2ndt=Ni0N1j0N2ndti=1stt/sCi0N1j0N1i=1stt/sC
353 352 com23 φi0N1j0N2ndti=1stt/sC2ndt=Ni0N1j0N1i=1stt/sC
354 353 imp φi0N1j0N2ndti=1stt/sC2ndt=Ni0N1j0N1i=1stt/sC
355 354 adantrd φi0N1j0N2ndti=1stt/sC2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N1i=1stt/sC
356 355 pm4.71rd φi0N1j0N2ndti=1stt/sC2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N1i=1stt/sC2ndt=N1st1sttN=02nd1sttN=N
357 an12 i0N1j0N1i=1stt/sC2ndt=N1st1sttN=02nd1sttN=N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
358 3anass i0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
359 358 anbi2i 2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
360 357 359 bitr4i i0N1j0N1i=1stt/sC2ndt=N1st1sttN=02nd1sttN=N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
361 356 360 bitrdi φi0N1j0N2ndti=1stt/sC2ndt=N1st1sttN=02nd1sttN=N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
362 361 notbid φi0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=N¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
363 362 pm5.32da φi0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1stt/sC¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
364 363 adantr φt0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N2ndti=1stt/sC¬2ndt=N1st1sttN=02nd1sttN=Ni0N1j0N2ndti=1stt/sC¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
365 231 345 364 3bitr3d φt0..^K1N×f|f:1N1-1 onto1N×0Nx0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKi0N1j0N2ndti=1stt/sC¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
366 365 rabbidva φt0..^K1N×f|f:1N1-1 onto1N×0N|x0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
367 iunrab x0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N|x0K1N0N1x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
368 difrab t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sC¬2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
369 366 367 368 3eqtr4g φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
370 369 fveq2d φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
371 32 33 mp1i φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKFin
372 simpl x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
373 372 a1i t0..^K1N×f|f:1N1-1 onto1N×0Nx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
374 373 ss2rabi t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKt0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
375 374 sseli st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKst0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
376 fveq2 t=s2ndt=2nds
377 376 breq2d t=sy<2ndty<2nds
378 377 ifbid t=sify<2ndtyy+1=ify<2ndsyy+1
379 378 csbeq1d t=sify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndsyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0
380 2fveq3 t=s1st1stt=1st1sts
381 2fveq3 t=s2nd1stt=2nd1sts
382 381 imaeq1d t=s2nd1stt1j=2nd1sts1j
383 382 xpeq1d t=s2nd1stt1j×1=2nd1sts1j×1
384 381 imaeq1d t=s2nd1sttj+1N=2nd1stsj+1N
385 384 xpeq1d t=s2nd1sttj+1N×0=2nd1stsj+1N×0
386 383 385 uneq12d t=s2nd1stt1j×12nd1sttj+1N×0=2nd1sts1j×12nd1stsj+1N×0
387 380 386 oveq12d t=s1st1stt+f2nd1stt1j×12nd1sttj+1N×0=1st1sts+f2nd1sts1j×12nd1stsj+1N×0
388 387 csbeq2dv t=sify<2ndsyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0
389 379 388 eqtrd t=sify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0
390 389 mpteq2dv t=sy0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0=y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0
391 390 eqeq2d t=sx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0x=y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0
392 eqcom x=y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
393 391 392 bitrdi t=sx=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
394 393 elrab st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0s0..^K1N×f|f:1N1-1 onto1N×0Ny0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
395 394 simprbi st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×0y0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
396 375 395 syl st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKy0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
397 396 rgen st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKy0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
398 397 rgenw x0K1N0N1st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKy0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=x
399 invdisj x0K1N0N1st0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnKy0N1ify<2ndsyy+1/j1st1sts+f2nd1sts1j×12nd1stsj+1N×0=xDisjx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
400 398 399 mp1i φDisjx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
401 13 371 400 hashiun φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=x0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
402 370 401 eqtr3d φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=x0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK
403 fo1st 1st:VontoV
404 fofun 1st:VontoVFun1st
405 403 404 ax-mp Fun1st
406 ssv t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=NV
407 fof 1st:VontoV1st:VV
408 403 407 ax-mp 1st:VV
409 408 fdmi dom1st=V
410 406 409 sseqtrri t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ndom1st
411 fores Fun1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ndom1st1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nonto1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
412 405 410 411 mp2an 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nonto1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
413 fveqeq2 t=x2ndt=N2ndx=N
414 fveq2 t=x1stt=1stx
415 414 csbeq1d t=x1stt/sC=1stx/sC
416 415 eqeq2d t=xi=1stt/sCi=1stx/sC
417 416 rexbidv t=xj0N1i=1stt/sCj0N1i=1stx/sC
418 417 ralbidv t=xi0N1j0N1i=1stt/sCi0N1j0N1i=1stx/sC
419 2fveq3 t=x1st1stt=1st1stx
420 419 fveq1d t=x1st1sttN=1st1stxN
421 420 eqeq1d t=x1st1sttN=01st1stxN=0
422 2fveq3 t=x2nd1stt=2nd1stx
423 422 fveq1d t=x2nd1sttN=2nd1stxN
424 423 eqeq1d t=x2nd1sttN=N2nd1stxN=N
425 418 421 424 3anbi123d t=xi0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N
426 413 425 anbi12d t=x2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N
427 426 rexrab xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=sx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s
428 xp1st x0..^K1N×f|f:1N1-1 onto1N×0N1stx0..^K1N×f|f:1N1-1 onto1N
429 428 anim1i x0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N
430 eleq1 1stx=s1stx0..^K1N×f|f:1N1-1 onto1Ns0..^K1N×f|f:1N1-1 onto1N
431 csbeq1a s=1stxC=1stx/sC
432 431 eqcoms 1stx=sC=1stx/sC
433 432 eqcomd 1stx=s1stx/sC=C
434 433 eqeq2d 1stx=si=1stx/sCi=C
435 434 rexbidv 1stx=sj0N1i=1stx/sCj0N1i=C
436 435 ralbidv 1stx=si0N1j0N1i=1stx/sCi0N1j0N1i=C
437 fveq2 1stx=s1st1stx=1sts
438 437 fveq1d 1stx=s1st1stxN=1stsN
439 438 eqeq1d 1stx=s1st1stxN=01stsN=0
440 fveq2 1stx=s2nd1stx=2nds
441 440 fveq1d 1stx=s2nd1stxN=2ndsN
442 441 eqeq1d 1stx=s2nd1stxN=N2ndsN=N
443 436 439 442 3anbi123d 1stx=si0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=Ni0N1j0N1i=C1stsN=02ndsN=N
444 430 443 anbi12d 1stx=s1stx0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=Ns0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
445 429 444 syl5ibcom x0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
446 445 adantrl x0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
447 446 expimpd x0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
448 447 rexlimiv x0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
449 nn0fz0 N0N0N
450 175 449 sylib φN0N
451 opelxpi s0..^K1N×f|f:1N1-1 onto1NN0NsN0..^K1N×f|f:1N1-1 onto1N×0N
452 450 451 sylan2 s0..^K1N×f|f:1N1-1 onto1NφsN0..^K1N×f|f:1N1-1 onto1N×0N
453 452 ancoms φs0..^K1N×f|f:1N1-1 onto1NsN0..^K1N×f|f:1N1-1 onto1N×0N
454 opelxp2 sN0..^K1N×f|f:1N1-1 onto1N×0NN0N
455 op2ndg sVN0N2ndsN=N
456 455 biantrurd sVN0Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N
457 op1stg sVN0N1stsN=s
458 csbeq1a s=1stsNC=1stsN/sC
459 458 eqcoms 1stsN=sC=1stsN/sC
460 459 eqcomd 1stsN=s1stsN/sC=C
461 457 460 syl sVN0N1stsN/sC=C
462 461 eqeq2d sVN0Ni=1stsN/sCi=C
463 462 rexbidv sVN0Nj0N1i=1stsN/sCj0N1i=C
464 463 ralbidv sVN0Ni0N1j0N1i=1stsN/sCi0N1j0N1i=C
465 457 fveq2d sVN0N1st1stsN=1sts
466 465 fveq1d sVN0N1st1stsNN=1stsN
467 466 eqeq1d sVN0N1st1stsNN=01stsN=0
468 457 fveq2d sVN0N2nd1stsN=2nds
469 468 fveq1d sVN0N2nd1stsNN=2ndsN
470 469 eqeq1d sVN0N2nd1stsNN=N2ndsN=N
471 464 467 470 3anbi123d sVN0Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=Ni0N1j0N1i=C1stsN=02ndsN=N
472 457 biantrud sVN0N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=s
473 456 471 472 3bitr3d sVN0Ni0N1j0N1i=C1stsN=02ndsN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=s
474 49 454 473 sylancr sN0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N1i=C1stsN=02ndsN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=s
475 474 biimpa sN0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N1i=C1stsN=02ndsN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=s
476 fveqeq2 x=sN2ndx=N2ndsN=N
477 fveq2 x=sN1stx=1stsN
478 477 csbeq1d x=sN1stx/sC=1stsN/sC
479 478 eqeq2d x=sNi=1stx/sCi=1stsN/sC
480 479 rexbidv x=sNj0N1i=1stx/sCj0N1i=1stsN/sC
481 480 ralbidv x=sNi0N1j0N1i=1stx/sCi0N1j0N1i=1stsN/sC
482 2fveq3 x=sN1st1stx=1st1stsN
483 482 fveq1d x=sN1st1stxN=1st1stsNN
484 483 eqeq1d x=sN1st1stxN=01st1stsNN=0
485 2fveq3 x=sN2nd1stx=2nd1stsN
486 485 fveq1d x=sN2nd1stxN=2nd1stsNN
487 486 eqeq1d x=sN2nd1stxN=N2nd1stsNN=N
488 481 484 487 3anbi123d x=sNi0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N
489 476 488 anbi12d x=sN2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N
490 fveqeq2 x=sN1stx=s1stsN=s
491 489 490 anbi12d x=sN2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=s
492 491 rspcev sN0..^K1N×f|f:1N1-1 onto1N×0N2ndsN=Ni0N1j0N1i=1stsN/sC1st1stsNN=02nd1stsNN=N1stsN=sx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s
493 475 492 syldan sN0..^K1N×f|f:1N1-1 onto1N×0Ni0N1j0N1i=C1stsN=02ndsN=Nx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s
494 453 493 sylan φs0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=Nx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s
495 494 expl φs0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=Nx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=s
496 448 495 impbid2 φx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ni0N1j0N1i=1stx/sC1st1stxN=02nd1stxN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
497 427 496 bitrid φxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=ss0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
498 497 abbidv φs|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=s=s|s0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
499 dfimafn Fun1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ndom1st1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=y|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=y
500 405 410 499 mp2an 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=y|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=y
501 nfv s2ndt=N
502 nfcv _s0N1
503 nfcsb1v _s1stt/sC
504 503 nfeq2 si=1stt/sC
505 502 504 nfrexw sj0N1i=1stt/sC
506 502 505 nfralw si0N1j0N1i=1stt/sC
507 nfv s1st1sttN=0
508 nfv s2nd1sttN=N
509 506 507 508 nf3an si0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
510 501 509 nfan s2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
511 nfcv _s0..^K1N×f|f:1N1-1 onto1N×0N
512 510 511 nfrabw _st0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N
513 nfv s1stx=y
514 512 513 nfrexw sxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=y
515 nfv yxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=s
516 eqeq2 y=s1stx=y1stx=s
517 516 rexbidv y=sxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=yxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=s
518 514 515 517 cbvabw y|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=y=s|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=s
519 500 518 eqtri 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s|xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=s
520 df-rab s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N=s|s0..^K1N×f|f:1N1-1 onto1Ni0N1j0N1i=C1stsN=02ndsN=N
521 498 519 520 3eqtr4g φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
522 foeq3 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nonto1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
523 521 522 syl φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nonto1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
524 412 523 mpbii φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
525 fof 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
526 524 525 syl φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
527 fvres xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stx
528 fvres yt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ny=1sty
529 527 528 eqeqan12d xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ny1stx=1sty
530 simpl 2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N2ndt=N
531 530 a1i t0..^K1N×f|f:1N1-1 onto1N×0N2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N2ndt=N
532 531 ss2rabi t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=N
533 532 sseli xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=N
534 413 elrab xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Nx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=N
535 533 534 sylib xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx0..^K1N×f|f:1N1-1 onto1N×0N2ndx=N
536 532 sseli yt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=N
537 fveqeq2 t=y2ndt=N2ndy=N
538 537 elrab yt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndy=N
539 536 538 sylib yt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndy=N
540 eqtr3 2ndx=N2ndy=N2ndx=2ndy
541 xpopth x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N1stx=1sty2ndx=2ndyx=y
542 541 biimpd x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N1stx=1sty2ndx=2ndyx=y
543 542 ancomsd x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndx=2ndy1stx=1styx=y
544 543 expdimp x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndx=2ndy1stx=1styx=y
545 540 544 sylan2 x0..^K1N×f|f:1N1-1 onto1N×0Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndx=N2ndy=N1stx=1styx=y
546 545 an4s x0..^K1N×f|f:1N1-1 onto1N×0N2ndx=Ny0..^K1N×f|f:1N1-1 onto1N×0N2ndy=N1stx=1styx=y
547 535 539 546 syl2an xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stx=1styx=y
548 529 547 sylbid xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyx=y
549 548 rgen2 xt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyx=y
550 526 549 jctir φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=Nxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyx=y
551 dff13 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=Nxt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nx=1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nyx=y
552 550 551 sylibr φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
553 df-f1o 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Nontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
554 552 524 553 sylanbrc φ1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
555 rabfi 0..^K1N×f|f:1N1-1 onto1N×0NFint0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=NFin
556 32 555 ax-mp t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=NFin
557 556 elexi t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=NV
558 557 f1oen 1stt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N:t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N1-1 ontos0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=Nt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
559 554 558 syl φt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
560 rabfi 0..^K1N×f|f:1N1-1 onto1NFins0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=NFin
561 29 560 ax-mp s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=NFin
562 hashen t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=NFins0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=NFint0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=Nt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
563 556 561 562 mp2an t0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=Nt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=Ns0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
564 559 563 sylibr φt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=s0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
565 564 oveq2d φt0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCt0..^K1N×f|f:1N1-1 onto1N×0N|2ndt=Ni0N1j0N1i=1stt/sC1st1sttN=02nd1sttN=N=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
566 205 402 565 3eqtr3d φx0K1N0N1t0..^K1N×f|f:1N1-1 onto1N×0N|x=y0N1ify<2ndtyy+1/j1st1stt+f2nd1stt1j×12nd1sttj+1N×00N1ranpranxBn1Npranxpn0pranxpnK=t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N
567 168 566 breqtrd φ2t0..^K1N×f|f:1N1-1 onto1N×0N|i0N1j0N2ndti=1stt/sCs0..^K1N×f|f:1N1-1 onto1N|i0N1j0N1i=C1stsN=02ndsN=N