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 = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
poimirlem28.2 φ p : 1 N 0 K B 0 N
Assertion poimirlem26 φ 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem28.1 p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C
3 poimirlem28.2 φ p : 1 N 0 K B 0 N
4 fzofi 0 ..^ K Fin
5 fzfi 1 N Fin
6 mapfi 0 ..^ K Fin 1 N Fin 0 ..^ K 1 N Fin
7 4 5 6 mp2an 0 ..^ K 1 N Fin
8 mapfi 1 N Fin 1 N Fin 1 N 1 N Fin
9 5 5 8 mp2an 1 N 1 N Fin
10 f1of f : 1 N 1-1 onto 1 N f : 1 N 1 N
11 10 ss2abi f | f : 1 N 1-1 onto 1 N f | f : 1 N 1 N
12 ovex 1 N V
13 12 12 mapval 1 N 1 N = f | f : 1 N 1 N
14 11 13 sseqtrri f | f : 1 N 1-1 onto 1 N 1 N 1 N
15 ssfi 1 N 1 N Fin f | f : 1 N 1-1 onto 1 N 1 N 1 N f | f : 1 N 1-1 onto 1 N Fin
16 9 14 15 mp2an f | f : 1 N 1-1 onto 1 N Fin
17 7 16 pm3.2i 0 ..^ K 1 N Fin f | f : 1 N 1-1 onto 1 N Fin
18 xpfi 0 ..^ K 1 N Fin f | f : 1 N 1-1 onto 1 N Fin 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin
19 17 18 mp1i φ 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin
20 2z 2
21 20 a1i φ 2
22 snfi x Fin
23 fzfi 0 N Fin
24 rabfi 0 N Fin y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin
25 23 24 ax-mp y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin
26 xpfi x Fin y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin
27 22 25 26 mp2an x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin
28 hashcl x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C 0
29 27 28 ax-mp x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C 0
30 29 nn0zi x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
31 30 a1i φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
32 1 ad2antrr φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C N
33 nfv j p = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0
34 nfcsb1v _ j k / j t / s C
35 34 nfeq2 j B = k / j t / s C
36 33 35 nfim j p = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0 B = k / j t / s C
37 oveq2 j = k 1 j = 1 k
38 37 imaeq2d j = k 2 nd t 1 j = 2 nd t 1 k
39 38 xpeq1d j = k 2 nd t 1 j × 1 = 2 nd t 1 k × 1
40 oveq1 j = k j + 1 = k + 1
41 40 oveq1d j = k j + 1 N = k + 1 N
42 41 imaeq2d j = k 2 nd t j + 1 N = 2 nd t k + 1 N
43 42 xpeq1d j = k 2 nd t j + 1 N × 0 = 2 nd t k + 1 N × 0
44 39 43 uneq12d j = k 2 nd t 1 j × 1 2 nd t j + 1 N × 0 = 2 nd t 1 k × 1 2 nd t k + 1 N × 0
45 44 oveq2d j = k 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0
46 45 eqeq2d j = k p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 p = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0
47 csbeq1a j = k t / s C = k / j t / s C
48 47 eqeq2d j = k B = t / s C B = k / j t / s C
49 46 48 imbi12d j = k p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 B = t / s C p = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0 B = k / j t / s C
50 nfv s p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0
51 nfcsb1v _ s t / s C
52 51 nfeq2 s B = t / s C
53 50 52 nfim s p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 B = t / s C
54 fveq2 s = t 1 st s = 1 st t
55 fveq2 s = t 2 nd s = 2 nd t
56 55 imaeq1d s = t 2 nd s 1 j = 2 nd t 1 j
57 56 xpeq1d s = t 2 nd s 1 j × 1 = 2 nd t 1 j × 1
58 55 imaeq1d s = t 2 nd s j + 1 N = 2 nd t j + 1 N
59 58 xpeq1d s = t 2 nd s j + 1 N × 0 = 2 nd t j + 1 N × 0
60 57 59 uneq12d s = t 2 nd s 1 j × 1 2 nd s j + 1 N × 0 = 2 nd t 1 j × 1 2 nd t j + 1 N × 0
61 54 60 oveq12d s = t 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0
62 61 eqeq2d s = t p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0
63 csbeq1a s = t C = t / s C
64 63 eqeq2d s = t B = C B = t / s C
65 62 64 imbi12d s = t p = 1 st s + f 2 nd s 1 j × 1 2 nd s j + 1 N × 0 B = C p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 B = t / s C
66 53 65 2 chvarfv p = 1 st t + f 2 nd t 1 j × 1 2 nd t j + 1 N × 0 B = t / s C
67 36 49 66 chvarfv p = 1 st t + f 2 nd t 1 k × 1 2 nd t k + 1 N × 0 B = k / j t / s C
68 3 ad4ant14 φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C p : 1 N 0 K B 0 N
69 xp1st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st x 0 ..^ K 1 N
70 elmapi 1 st x 0 ..^ K 1 N 1 st x : 1 N 0 ..^ K
71 69 70 syl x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 1 st x : 1 N 0 ..^ K
72 71 ad2antlr φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C 1 st x : 1 N 0 ..^ K
73 xp2nd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd x f | f : 1 N 1-1 onto 1 N
74 fvex 2 nd x V
75 f1oeq1 f = 2 nd x f : 1 N 1-1 onto 1 N 2 nd x : 1 N 1-1 onto 1 N
76 74 75 elab 2 nd x f | f : 1 N 1-1 onto 1 N 2 nd x : 1 N 1-1 onto 1 N
77 73 76 sylib x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 nd x : 1 N 1-1 onto 1 N
78 77 ad2antlr φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C 2 nd x : 1 N 1-1 onto 1 N
79 nfcv _ j N
80 nfcv _ j x
81 80 34 nfcsbw _ j x / t k / j t / s C
82 79 81 nfne j N x / t k / j t / s C
83 nfcv _ t C
84 83 51 63 cbvcsbw x / s C = x / t t / s C
85 47 csbeq2dv j = k x / t t / s C = x / t k / j t / s C
86 84 85 syl5eq j = k x / s C = x / t k / j t / s C
87 86 neeq2d j = k N x / s C N x / t k / j t / s C
88 82 87 rspc k 0 N j 0 N N x / s C N x / t k / j t / s C
89 88 impcom j 0 N N x / s C k 0 N N x / t k / j t / s C
90 89 adantll φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C k 0 N N x / t k / j t / s C
91 1st2nd2 x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x = 1 st x 2 nd x
92 91 csbeq1d x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x / t k / j t / s C = 1 st x 2 nd x / t k / j t / s C
93 92 ad3antlr φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C k 0 N x / t k / j t / s C = 1 st x 2 nd x / t k / j t / s C
94 90 93 neeqtrd φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C k 0 N N 1 st x 2 nd x / t k / j t / s C
95 32 67 68 72 78 94 poimirlem25 φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C 2 y 0 N | i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C
96 nfv k i = x / s C
97 81 nfeq2 j i = x / t k / j t / s C
98 86 eqeq2d j = k i = x / s C i = x / t k / j t / s C
99 96 97 98 cbvrexw j 0 N y i = x / s C k 0 N y i = x / t k / j t / s C
100 92 eqeq2d x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i = x / t k / j t / s C i = 1 st x 2 nd x / t k / j t / s C
101 100 rexbidv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k 0 N y i = x / t k / j t / s C k 0 N y i = 1 st x 2 nd x / t k / j t / s C
102 99 101 syl5rbb x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k 0 N y i = 1 st x 2 nd x / t k / j t / s C j 0 N y i = x / s C
103 102 ralbidv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C i 0 N 1 j 0 N y i = x / s C
104 iba j 0 N N x / s C i 0 N 1 j 0 N y i = x / s C i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
105 103 104 sylan9bb x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
106 105 rabbidv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C y 0 N | i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C = y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
107 106 fveq2d x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C y 0 N | i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C = y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
108 107 adantll φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C y 0 N | i 0 N 1 k 0 N y i = 1 st x 2 nd x / t k / j t / s C = y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
109 95 108 breqtrd φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C 2 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
110 109 ex φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N j 0 N N x / s C 2 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
111 dvds0 2 2 0
112 20 111 ax-mp 2 0
113 hash0 = 0
114 112 113 breqtrri 2
115 simpr i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C j 0 N N x / s C
116 115 con3i ¬ j 0 N N x / s C ¬ i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
117 116 ralrimivw ¬ j 0 N N x / s C y 0 N ¬ i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
118 rabeq0 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = y 0 N ¬ i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
119 117 118 sylibr ¬ j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C =
120 119 fveq2d ¬ j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C =
121 114 120 breqtrrid ¬ j 0 N N x / s C 2 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
122 110 121 pm2.61d1 φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
123 hashxp x Fin y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = x y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
124 22 25 123 mp2an x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = x y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
125 vex x V
126 hashsng x V x = 1
127 125 126 ax-mp x = 1
128 127 oveq1i x y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = 1 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
129 hashcl y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C 0
130 25 129 ax-mp y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C 0
131 130 nn0cni y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
132 131 mulid2i 1 y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
133 124 128 132 3eqtri x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
134 122 133 breqtrrdi φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N 2 x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
135 19 21 31 134 fsumdvds φ 2 x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
136 7 16 18 mp2an 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin
137 xpfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin 0 N Fin 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin
138 136 23 137 mp2an 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin
139 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin
140 138 139 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin
141 1 nncnd φ N
142 npcan1 N N - 1 + 1 = N
143 141 142 syl φ N - 1 + 1 = N
144 nnm1nn0 N N 1 0
145 1 144 syl φ N 1 0
146 145 nn0zd φ N 1
147 uzid N 1 N 1 N 1
148 peano2uz N 1 N 1 N - 1 + 1 N 1
149 146 147 148 3syl φ N - 1 + 1 N 1
150 143 149 eqeltrrd φ N N 1
151 fzss2 N N 1 0 N 1 0 N
152 ssralv 0 N 1 0 N i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C
153 150 151 152 3syl φ i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C
154 153 adantr φ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C
155 raldifb j 0 N j 2 nd t ¬ i = 1 st t / s C j 0 N 2 nd t ¬ i = 1 st t / s C
156 nfv j φ
157 nfcsb1v _ j 2 nd t / j 1 st t / s C
158 157 nfeq2 j N = 2 nd t / j 1 st t / s C
159 156 158 nfan j φ N = 2 nd t / j 1 st t / s C
160 nfv j i 0 N 1
161 159 160 nfan j φ N = 2 nd t / j 1 st t / s C i 0 N 1
162 nnel ¬ j 2 nd t j 2 nd t
163 velsn j 2 nd t j = 2 nd t
164 162 163 bitri ¬ j 2 nd t j = 2 nd t
165 csbeq1a j = 2 nd t 1 st t / s C = 2 nd t / j 1 st t / s C
166 165 eqeq2d j = 2 nd t N = 1 st t / s C N = 2 nd t / j 1 st t / s C
167 166 biimparc N = 2 nd t / j 1 st t / s C j = 2 nd t N = 1 st t / s C
168 1 nnred φ N
169 168 ltm1d φ N 1 < N
170 145 nn0red φ N 1
171 170 168 ltnled φ N 1 < N ¬ N N 1
172 169 171 mpbid φ ¬ N N 1
173 elfzle2 N 0 N 1 N N 1
174 172 173 nsyl φ ¬ N 0 N 1
175 eleq1 i = N i 0 N 1 N 0 N 1
176 175 notbid i = N ¬ i 0 N 1 ¬ N 0 N 1
177 174 176 syl5ibrcom φ i = N ¬ i 0 N 1
178 177 con2d φ i 0 N 1 ¬ i = N
179 178 imp φ i 0 N 1 ¬ i = N
180 eqeq2 N = 1 st t / s C i = N i = 1 st t / s C
181 180 notbid N = 1 st t / s C ¬ i = N ¬ i = 1 st t / s C
182 179 181 syl5ibcom φ i 0 N 1 N = 1 st t / s C ¬ i = 1 st t / s C
183 167 182 syl5 φ i 0 N 1 N = 2 nd t / j 1 st t / s C j = 2 nd t ¬ i = 1 st t / s C
184 183 expdimp φ i 0 N 1 N = 2 nd t / j 1 st t / s C j = 2 nd t ¬ i = 1 st t / s C
185 184 an32s φ N = 2 nd t / j 1 st t / s C i 0 N 1 j = 2 nd t ¬ i = 1 st t / s C
186 164 185 syl5bi φ N = 2 nd t / j 1 st t / s C i 0 N 1 ¬ j 2 nd t ¬ i = 1 st t / s C
187 idd φ N = 2 nd t / j 1 st t / s C i 0 N 1 ¬ i = 1 st t / s C ¬ i = 1 st t / s C
188 186 187 jad φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 2 nd t ¬ i = 1 st t / s C ¬ i = 1 st t / s C
189 188 adantr φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 0 N j 2 nd t ¬ i = 1 st t / s C ¬ i = 1 st t / s C
190 161 189 ralimdaa φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 0 N j 2 nd t ¬ i = 1 st t / s C j 0 N ¬ i = 1 st t / s C
191 155 190 syl5bir φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 0 N 2 nd t ¬ i = 1 st t / s C j 0 N ¬ i = 1 st t / s C
192 191 con3d φ N = 2 nd t / j 1 st t / s C i 0 N 1 ¬ j 0 N ¬ i = 1 st t / s C ¬ j 0 N 2 nd t ¬ i = 1 st t / s C
193 dfrex2 j 0 N i = 1 st t / s C ¬ j 0 N ¬ i = 1 st t / s C
194 dfrex2 j 0 N 2 nd t i = 1 st t / s C ¬ j 0 N 2 nd t ¬ i = 1 st t / s C
195 192 193 194 3imtr4g φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C j 0 N 2 nd t i = 1 st t / s C
196 195 ralimdva φ N = 2 nd t / j 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
197 154 196 syld φ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
198 197 expimpd φ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
199 198 adantr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
200 199 ss2rabdv φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
201 hashssdif t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
202 140 200 201 sylancr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
203 xp2nd t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd t 0 N
204 df-ne N 1 st t / s C ¬ N = 1 st t / s C
205 204 ralbii j 0 N N 1 st t / s C j 0 N ¬ N = 1 st t / s C
206 ralnex j 0 N ¬ N = 1 st t / s C ¬ j 0 N N = 1 st t / s C
207 205 206 bitri j 0 N N 1 st t / s C ¬ j 0 N N = 1 st t / s C
208 1 nnnn0d φ N 0
209 nn0uz 0 = 0
210 208 209 eleqtrdi φ N 0
211 143 210 eqeltrd φ N - 1 + 1 0
212 fzsplit2 N - 1 + 1 0 N N 1 0 N = 0 N 1 N - 1 + 1 N
213 211 150 212 syl2anc φ 0 N = 0 N 1 N - 1 + 1 N
214 143 oveq1d φ N - 1 + 1 N = N N
215 1 nnzd φ N
216 fzsn N N N = N
217 215 216 syl φ N N = N
218 214 217 eqtrd φ N - 1 + 1 N = N
219 218 uneq2d φ 0 N 1 N - 1 + 1 N = 0 N 1 N
220 213 219 eqtrd φ 0 N = 0 N 1 N
221 220 raleqdv φ i 0 N j 0 N i = 1 st t / s C i 0 N 1 N j 0 N i = 1 st t / s C
222 ralunb i 0 N 1 N j 0 N i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C i N j 0 N i = 1 st t / s C
223 difss 0 N 2 nd t 0 N
224 ssrexv 0 N 2 nd t 0 N j 0 N 2 nd t i = 1 st t / s C j 0 N i = 1 st t / s C
225 223 224 ax-mp j 0 N 2 nd t i = 1 st t / s C j 0 N i = 1 st t / s C
226 225 ralimi i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C
227 226 biantrurd i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i N j 0 N i = 1 st t / s C i 0 N 1 j 0 N i = 1 st t / s C i N j 0 N i = 1 st t / s C
228 222 227 bitr4id i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 N j 0 N i = 1 st t / s C i N j 0 N i = 1 st t / s C
229 221 228 sylan9bb φ i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N j 0 N i = 1 st t / s C i N j 0 N i = 1 st t / s C
230 229 adantlr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N j 0 N i = 1 st t / s C i N j 0 N i = 1 st t / s C
231 nn0fz0 N 0 N 0 N
232 208 231 sylib φ N 0 N
233 232 ad2antrr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C N 0 N
234 eqeq1 i = N i = 1 st t / s C N = 1 st t / s C
235 234 rexbidv i = N j 0 N i = 1 st t / s C j 0 N N = 1 st t / s C
236 235 rspcva N 0 N i 0 N j 0 N i = 1 st t / s C j 0 N N = 1 st t / s C
237 nfv j φ 2 nd t 0 N
238 nfcv _ j 0 N 1
239 nfre1 j j 0 N 2 nd t i = 1 st t / s C
240 238 239 nfralw j i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
241 237 240 nfan j φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C
242 eleq1 N = 1 st t / s C N 0 N 1 1 st t / s C 0 N 1
243 242 notbid N = 1 st t / s C ¬ N 0 N 1 ¬ 1 st t / s C 0 N 1
244 174 243 syl5ibcom φ N = 1 st t / s C ¬ 1 st t / s C 0 N 1
245 244 ad3antrrr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C ¬ 1 st t / s C 0 N 1
246 eldifsn j 0 N 2 nd t j 0 N j 2 nd t
247 diffi 0 N Fin 0 N 2 nd t Fin
248 23 247 ax-mp 0 N 2 nd t Fin
249 ssrab2 j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t
250 ssdomg 0 N 2 nd t Fin j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t
251 248 249 250 mp2 j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t
252 hashdifsn 0 N Fin 2 nd t 0 N 0 N 2 nd t = 0 N 1
253 23 252 mpan 2 nd t 0 N 0 N 2 nd t = 0 N 1
254 1cnd φ 1
255 141 254 254 addsubd φ N + 1 - 1 = N - 1 + 1
256 hashfz0 N 0 0 N = N + 1
257 208 256 syl φ 0 N = N + 1
258 257 oveq1d φ 0 N 1 = N + 1 - 1
259 hashfz0 N 1 0 0 N 1 = N - 1 + 1
260 145 259 syl φ 0 N 1 = N - 1 + 1
261 255 258 260 3eqtr4d φ 0 N 1 = 0 N 1
262 253 261 sylan9eqr φ 2 nd t 0 N 0 N 2 nd t = 0 N 1
263 fzfi 0 N 1 Fin
264 hashen 0 N 2 nd t Fin 0 N 1 Fin 0 N 2 nd t = 0 N 1 0 N 2 nd t 0 N 1
265 248 263 264 mp2an 0 N 2 nd t = 0 N 1 0 N 2 nd t 0 N 1
266 262 265 sylib φ 2 nd t 0 N 0 N 2 nd t 0 N 1
267 rabfi 0 N 2 nd t Fin j 0 N 2 nd t | 1 st t / s C 0 N 1 Fin
268 248 267 ax-mp j 0 N 2 nd t | 1 st t / s C 0 N 1 Fin
269 eleq1 i = 1 st t / s C i 0 N 1 1 st t / s C 0 N 1
270 269 biimpac i 0 N 1 i = 1 st t / s C 1 st t / s C 0 N 1
271 rabid j j 0 N 2 nd t | 1 st t / s C 0 N 1 j 0 N 2 nd t 1 st t / s C 0 N 1
272 271 simplbi2com 1 st t / s C 0 N 1 j 0 N 2 nd t j j 0 N 2 nd t | 1 st t / s C 0 N 1
273 270 272 syl i 0 N 1 i = 1 st t / s C j 0 N 2 nd t j j 0 N 2 nd t | 1 st t / s C 0 N 1
274 273 impancom i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1
275 274 ancrd i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
276 275 expimpd i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
277 276 reximdv2 i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
278 271 simplbi j j 0 N 2 nd t | 1 st t / s C 0 N 1 j 0 N 2 nd t
279 274 pm4.71rd i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
280 df-mpt k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C = k i | k j 0 N 2 nd t | 1 st t / s C 0 N 1 i = k / j 1 st t / s C
281 nfv k j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
282 nfrab1 _ j j 0 N 2 nd t | 1 st t / s C 0 N 1
283 282 nfcri j k j 0 N 2 nd t | 1 st t / s C 0 N 1
284 nfcsb1v _ j k / j 1 st t / s C
285 284 nfeq2 j i = k / j 1 st t / s C
286 283 285 nfan j k j 0 N 2 nd t | 1 st t / s C 0 N 1 i = k / j 1 st t / s C
287 eleq1 j = k j j 0 N 2 nd t | 1 st t / s C 0 N 1 k j 0 N 2 nd t | 1 st t / s C 0 N 1
288 csbeq1a j = k 1 st t / s C = k / j 1 st t / s C
289 288 eqeq2d j = k i = 1 st t / s C i = k / j 1 st t / s C
290 287 289 anbi12d j = k j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C k j 0 N 2 nd t | 1 st t / s C 0 N 1 i = k / j 1 st t / s C
291 281 286 290 cbvopab1 j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C = k i | k j 0 N 2 nd t | 1 st t / s C 0 N 1 i = k / j 1 st t / s C
292 280 291 eqtr4i k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C = j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
293 292 breqi j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i j j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C i
294 df-br j j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C i j i j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
295 opabidw j i j i | j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
296 293 294 295 3bitri j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C
297 279 296 bitr4di i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
298 278 297 sylan2 i 0 N 1 j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
299 298 rexbidva i 0 N 1 j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
300 nfcv _ p j 0 N 2 nd t | 1 st t / s C 0 N 1
301 nfv p j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
302 nfcv _ j p
303 282 284 nfmpt _ j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C
304 nfcv _ j i
305 302 303 304 nfbr j p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
306 breq1 j = p j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
307 282 300 301 305 306 cbvrexfw j j 0 N 2 nd t | 1 st t / s C 0 N 1 j k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
308 299 307 syl6bb i 0 N 1 j j 0 N 2 nd t | 1 st t / s C 0 N 1 i = 1 st t / s C p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
309 277 308 sylibd i 0 N 1 j 0 N 2 nd t i = 1 st t / s C p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
310 309 ralimia i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
311 eqid k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C = k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C
312 nfcv _ j k
313 nfcv _ j 0 N 2 nd t
314 284 nfel1 j k / j 1 st t / s C 0 N 1
315 288 eleq1d j = k 1 st t / s C 0 N 1 k / j 1 st t / s C 0 N 1
316 312 313 314 315 elrabf k j 0 N 2 nd t | 1 st t / s C 0 N 1 k 0 N 2 nd t k / j 1 st t / s C 0 N 1
317 316 simprbi k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C 0 N 1
318 311 317 fmpti k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 1
319 310 318 jctil i 0 N 1 j 0 N 2 nd t i = 1 st t / s C k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 1 i 0 N 1 p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
320 dffo4 k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 onto 0 N 1 k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 1 i 0 N 1 p j 0 N 2 nd t | 1 st t / s C 0 N 1 p k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C i
321 319 320 sylibr i 0 N 1 j 0 N 2 nd t i = 1 st t / s C k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 onto 0 N 1
322 fodomfi j 0 N 2 nd t | 1 st t / s C 0 N 1 Fin k j 0 N 2 nd t | 1 st t / s C 0 N 1 k / j 1 st t / s C : j 0 N 2 nd t | 1 st t / s C 0 N 1 onto 0 N 1 0 N 1 j 0 N 2 nd t | 1 st t / s C 0 N 1
323 268 321 322 sylancr i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 0 N 1 j 0 N 2 nd t | 1 st t / s C 0 N 1
324 endomtr 0 N 2 nd t 0 N 1 0 N 1 j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1
325 266 323 324 syl2an φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1
326 sbth j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1 j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t
327 251 325 326 sylancr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t
328 fisseneq 0 N 2 nd t Fin j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1 0 N 2 nd t j 0 N 2 nd t | 1 st t / s C 0 N 1 = 0 N 2 nd t
329 248 249 327 328 mp3an12i φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N 2 nd t | 1 st t / s C 0 N 1 = 0 N 2 nd t
330 329 eleq2d φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j j 0 N 2 nd t | 1 st t / s C 0 N 1 j 0 N 2 nd t
331 330 biimpar φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N 2 nd t j j 0 N 2 nd t | 1 st t / s C 0 N 1
332 288 equcoms k = j 1 st t / s C = k / j 1 st t / s C
333 332 eqcomd k = j k / j 1 st t / s C = 1 st t / s C
334 333 eleq1d k = j k / j 1 st t / s C 0 N 1 1 st t / s C 0 N 1
335 334 317 vtoclga j j 0 N 2 nd t | 1 st t / s C 0 N 1 1 st t / s C 0 N 1
336 331 335 syl φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N 2 nd t 1 st t / s C 0 N 1
337 246 336 sylan2br φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N j 2 nd t 1 st t / s C 0 N 1
338 337 expr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N j 2 nd t 1 st t / s C 0 N 1
339 338 necon1bd φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N ¬ 1 st t / s C 0 N 1 j = 2 nd t
340 245 339 syld φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C j = 2 nd t
341 340 imp φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C j = 2 nd t
342 341 165 syl φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C 1 st t / s C = 2 nd t / j 1 st t / s C
343 eqtr N = 1 st t / s C 1 st t / s C = 2 nd t / j 1 st t / s C N = 2 nd t / j 1 st t / s C
344 343 ex N = 1 st t / s C 1 st t / s C = 2 nd t / j 1 st t / s C N = 2 nd t / j 1 st t / s C
345 344 adantl φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C 1 st t / s C = 2 nd t / j 1 st t / s C N = 2 nd t / j 1 st t / s C
346 342 345 mpd φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C N = 2 nd t / j 1 st t / s C
347 346 exp31 φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C N = 2 nd t / j 1 st t / s C
348 241 158 347 rexlimd φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C N = 2 nd t / j 1 st t / s C
349 236 348 syl5 φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C N 0 N i 0 N j 0 N i = 1 st t / s C N = 2 nd t / j 1 st t / s C
350 233 349 mpand φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N j 0 N i = 1 st t / s C N = 2 nd t / j 1 st t / s C
351 350 pm4.71rd φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N j 0 N i = 1 st t / s C N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
352 235 ralsng N i N j 0 N i = 1 st t / s C j 0 N N = 1 st t / s C
353 1 352 syl φ i N j 0 N i = 1 st t / s C j 0 N N = 1 st t / s C
354 353 ad2antrr φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i N j 0 N i = 1 st t / s C j 0 N N = 1 st t / s C
355 230 351 354 3bitr3rd φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N = 1 st t / s C N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
356 355 notbid φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ j 0 N N = 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
357 207 356 syl5bb φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
358 357 pm5.32da φ 2 nd t 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
359 203 358 sylan2 φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
360 359 rabbidva φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
361 nfv y t = x k
362 nfv y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
363 nfrab1 _ y y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
364 363 nfcri y k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
365 362 364 nfan y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
366 361 365 nfan y t = x k x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
367 nfv k t = x y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
368 opeq2 k = y x k = x y
369 368 eqeq2d k = y t = x k t = x y
370 eleq1 k = y k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
371 rabid y y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
372 370 371 syl6bb k = y k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
373 372 anbi2d k = y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
374 3anass x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
375 373 374 bitr4di k = y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
376 369 375 anbi12d k = y t = x k x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t = x y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
377 366 367 376 cbvexv1 k t = x k x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y t = x y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
378 377 exbii x k t = x k x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x y t = x y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
379 eliunxp t x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x k t = x k x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N k y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
380 elopab t x y | x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x y t = x y x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
381 378 379 380 3bitr4i t x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t x y | x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
382 381 eqriv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = x y | x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
383 vex y V
384 125 383 op2ndd t = x y 2 nd t = y
385 384 sneqd t = x y 2 nd t = y
386 385 difeq2d t = x y 0 N 2 nd t = 0 N y
387 125 383 op1std t = x y 1 st t = x
388 387 csbeq1d t = x y 1 st t / s C = x / s C
389 388 eqeq2d t = x y i = 1 st t / s C i = x / s C
390 386 389 rexeqbidv t = x y j 0 N 2 nd t i = 1 st t / s C j 0 N y i = x / s C
391 390 ralbidv t = x y i 0 N 1 j 0 N 2 nd t i = 1 st t / s C i 0 N 1 j 0 N y i = x / s C
392 388 neeq2d t = x y N 1 st t / s C N x / s C
393 392 ralbidv t = x y j 0 N N 1 st t / s C j 0 N N x / s C
394 391 393 anbi12d t = x y i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
395 394 rabxp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C = x y | x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N y 0 N i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
396 382 395 eqtr4i x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C j 0 N N 1 st t / s C
397 difrab t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C ¬ N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
398 360 396 397 3eqtr4g φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
399 398 fveq2d φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
400 27 a1i φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C Fin
401 inxp x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C = x t × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C
402 df-ne x t ¬ x = t
403 disjsn2 x t x t =
404 402 403 sylbir ¬ x = t x t =
405 404 xpeq1d ¬ x = t x t × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C = × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C
406 0xp × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
407 405 406 eqtrdi ¬ x = t x t × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
408 401 407 syl5eq ¬ x = t x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
409 408 orri x = t x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
410 409 rgen2w x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x = t x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
411 sneq x = t x = t
412 csbeq1 x = t x / s C = t / s C
413 412 eqeq2d x = t i = x / s C i = t / s C
414 413 rexbidv x = t j 0 N y i = x / s C j 0 N y i = t / s C
415 414 ralbidv x = t i 0 N 1 j 0 N y i = x / s C i 0 N 1 j 0 N y i = t / s C
416 412 neeq2d x = t N x / s C N t / s C
417 416 ralbidv x = t j 0 N N x / s C j 0 N N t / s C
418 415 417 anbi12d x = t i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C
419 418 rabbidv x = t y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C
420 411 419 xpeq12d x = t x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C
421 420 disjor Disj x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x = t x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C t × y 0 N | i 0 N 1 j 0 N y i = t / s C j 0 N N t / s C =
422 410 421 mpbir Disj x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
423 422 a1i φ Disj x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
424 19 400 423 hashiun φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
425 399 424 eqtr3d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C
426 fo1st 1 st : V onto V
427 fofun 1 st : V onto V Fun 1 st
428 426 427 ax-mp Fun 1 st
429 ssv t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C V
430 fof 1 st : V onto V 1 st : V V
431 426 430 ax-mp 1 st : V V
432 431 fdmi dom 1 st = V
433 429 432 sseqtrri t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C dom 1 st
434 fores Fun 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C dom 1 st 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
435 428 433 434 mp2an 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
436 fveq2 t = x 2 nd t = 2 nd x
437 436 csbeq1d t = x 2 nd t / j 1 st t / s C = 2 nd x / j 1 st t / s C
438 fveq2 t = x 1 st t = 1 st x
439 438 csbeq1d t = x 1 st t / s C = 1 st x / s C
440 439 csbeq2dv t = x 2 nd x / j 1 st t / s C = 2 nd x / j 1 st x / s C
441 437 440 eqtrd t = x 2 nd t / j 1 st t / s C = 2 nd x / j 1 st x / s C
442 441 eqeq2d t = x N = 2 nd t / j 1 st t / s C N = 2 nd x / j 1 st x / s C
443 439 eqeq2d t = x i = 1 st t / s C i = 1 st x / s C
444 443 rexbidv t = x j 0 N i = 1 st t / s C j 0 N i = 1 st x / s C
445 444 ralbidv t = x i 0 N j 0 N i = 1 st t / s C i 0 N j 0 N i = 1 st x / s C
446 442 445 anbi12d t = x N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
447 446 rexrab x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s
448 xp1st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
449 448 anim1i x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N j 0 N i = 1 st x / s C 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = 1 st x / s C
450 eleq1 1 st x = s 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
451 csbeq1a s = 1 st x C = 1 st x / s C
452 451 eqcoms 1 st x = s C = 1 st x / s C
453 452 eqcomd 1 st x = s 1 st x / s C = C
454 453 eqeq2d 1 st x = s i = 1 st x / s C i = C
455 454 rexbidv 1 st x = s j 0 N i = 1 st x / s C j 0 N i = C
456 455 ralbidv 1 st x = s i 0 N j 0 N i = 1 st x / s C i 0 N j 0 N i = C
457 450 456 anbi12d 1 st x = s 1 st x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = 1 st x / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
458 449 457 syl5ibcom x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N i 0 N j 0 N i = 1 st x / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
459 458 adantrl x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
460 459 expimpd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
461 460 rexlimiv x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
462 simplr φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N
463 ovex 0 N V
464 463 enref 0 N 0 N
465 phpreu 0 N Fin 0 N 0 N i 0 N j 0 N i = C i 0 N ∃! j 0 N i = C
466 23 464 465 mp2an i 0 N j 0 N i = C i 0 N ∃! j 0 N i = C
467 466 biimpi i 0 N j 0 N i = C i 0 N ∃! j 0 N i = C
468 eqeq1 i = N i = C N = C
469 468 reubidv i = N ∃! j 0 N i = C ∃! j 0 N N = C
470 469 rspcva N 0 N i 0 N ∃! j 0 N i = C ∃! j 0 N N = C
471 232 467 470 syl2an φ i 0 N j 0 N i = C ∃! j 0 N N = C
472 riotacl ∃! j 0 N N = C ι j 0 N | N = C 0 N
473 471 472 syl φ i 0 N j 0 N i = C ι j 0 N | N = C 0 N
474 473 adantlr φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C ι j 0 N | N = C 0 N
475 opelxpi s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N ι j 0 N | N = C 0 N s ι j 0 N | N = C 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
476 462 474 475 syl2anc φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C s ι j 0 N | N = C 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
477 riotasbc ∃! j 0 N N = C [˙ ι j 0 N | N = C / j]˙ N = C
478 471 477 syl φ i 0 N j 0 N i = C [˙ ι j 0 N | N = C / j]˙ N = C
479 riotaex ι j 0 N | N = C V
480 sbceq2g ι j 0 N | N = C V [˙ ι j 0 N | N = C / j]˙ N = C N = ι j 0 N | N = C / j C
481 479 480 ax-mp [˙ ι j 0 N | N = C / j]˙ N = C N = ι j 0 N | N = C / j C
482 478 481 sylib φ i 0 N j 0 N i = C N = ι j 0 N | N = C / j C
483 482 expcom i 0 N j 0 N i = C φ N = ι j 0 N | N = C / j C
484 483 imdistanri φ i 0 N j 0 N i = C N = ι j 0 N | N = C / j C i 0 N j 0 N i = C
485 484 adantlr φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C N = ι j 0 N | N = C / j C i 0 N j 0 N i = C
486 vex s V
487 486 479 op2ndd x = s ι j 0 N | N = C 2 nd x = ι j 0 N | N = C
488 487 csbeq1d x = s ι j 0 N | N = C 2 nd x / j C = ι j 0 N | N = C / j C
489 nfcv _ j s
490 nfriota1 _ j ι j 0 N | N = C
491 489 490 nfop _ j s ι j 0 N | N = C
492 491 nfeq2 j x = s ι j 0 N | N = C
493 486 479 op1std x = s ι j 0 N | N = C 1 st x = s
494 493 eqcomd x = s ι j 0 N | N = C s = 1 st x
495 494 451 syl x = s ι j 0 N | N = C C = 1 st x / s C
496 492 495 csbeq2d x = s ι j 0 N | N = C 2 nd x / j C = 2 nd x / j 1 st x / s C
497 488 496 eqtr3d x = s ι j 0 N | N = C ι j 0 N | N = C / j C = 2 nd x / j 1 st x / s C
498 497 eqeq2d x = s ι j 0 N | N = C N = ι j 0 N | N = C / j C N = 2 nd x / j 1 st x / s C
499 495 eqeq2d x = s ι j 0 N | N = C i = C i = 1 st x / s C
500 492 499 rexbid x = s ι j 0 N | N = C j 0 N i = C j 0 N i = 1 st x / s C
501 500 ralbidv x = s ι j 0 N | N = C i 0 N j 0 N i = C i 0 N j 0 N i = 1 st x / s C
502 498 501 anbi12d x = s ι j 0 N | N = C N = ι j 0 N | N = C / j C i 0 N j 0 N i = C N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
503 493 biantrud x = s ι j 0 N | N = C N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s
504 502 503 bitr2d x = s ι j 0 N | N = C N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s N = ι j 0 N | N = C / j C i 0 N j 0 N i = C
505 504 rspcev s ι j 0 N | N = C 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = ι j 0 N | N = C / j C i 0 N j 0 N i = C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s
506 476 485 505 syl2anc φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s
507 506 expl φ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s
508 461 507 impbid2 φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
509 447 508 syl5bb φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
510 509 abbidv φ s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s = s | s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
511 dfimafn Fun 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C dom 1 st 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = y
512 428 433 511 mp2an 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = y
513 nfcv _ s 2 nd t
514 nfcsb1v _ s 1 st t / s C
515 513 514 nfcsbw _ s 2 nd t / j 1 st t / s C
516 515 nfeq2 s N = 2 nd t / j 1 st t / s C
517 nfcv _ s 0 N
518 514 nfeq2 s i = 1 st t / s C
519 517 518 nfrex s j 0 N i = 1 st t / s C
520 517 519 nfralw s i 0 N j 0 N i = 1 st t / s C
521 516 520 nfan s N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
522 nfcv _ s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
523 521 522 nfrabw _ s t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C
524 nfv s 1 st x = y
525 523 524 nfrex s x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = y
526 nfv y x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s
527 eqeq2 y = s 1 st x = y 1 st x = s
528 527 rexbidv y = s x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = y x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s
529 525 526 528 cbvabw y | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = y = s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s
530 512 529 eqtri 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s | x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = s
531 df-rab s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C = s | s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N i 0 N j 0 N i = C
532 510 530 531 3eqtr4g φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
533 foeq3 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
534 532 533 syl φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
535 435 534 mpbii φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
536 fof 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
537 535 536 syl φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
538 fvres x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st x
539 fvres y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y = 1 st y
540 538 539 eqeqan12d x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y 1 st x = 1 st y
541 540 adantl φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y 1 st x = 1 st y
542 446 elrab x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
543 xp2nd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd x 0 N
544 543 anim1i x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
545 542 544 sylbi x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
546 simpl N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C N = 2 nd t / j 1 st t / s C
547 546 a1i t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C N = 2 nd t / j 1 st t / s C
548 547 ss2rabi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C
549 548 sseli y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C
550 fveq2 t = y 2 nd t = 2 nd y
551 550 csbeq1d t = y 2 nd t / j 1 st t / s C = 2 nd y / j 1 st t / s C
552 fveq2 t = y 1 st t = 1 st y
553 552 csbeq1d t = y 1 st t / s C = 1 st y / s C
554 553 csbeq2dv t = y 2 nd y / j 1 st t / s C = 2 nd y / j 1 st y / s C
555 551 554 eqtrd t = y 2 nd t / j 1 st t / s C = 2 nd y / j 1 st y / s C
556 555 eqeq2d t = y N = 2 nd t / j 1 st t / s C N = 2 nd y / j 1 st y / s C
557 556 elrab y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd y / j 1 st y / s C
558 xp2nd y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 2 nd y 0 N
559 558 anim1i y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N N = 2 nd y / j 1 st y / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
560 557 559 sylbi y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
561 549 560 syl y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
562 545 561 anim12i x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
563 an4 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
564 563 anbi2i i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
565 anass 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C
566 ancom 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C
567 565 566 bitr3i 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C
568 567 anbi1i 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
569 anass i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
570 568 569 bitri 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N N = 2 nd x / j 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C
571 anass i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
572 564 570 571 3bitr4i 2 nd x 0 N N = 2 nd x / j 1 st x / s C i 0 N j 0 N i = 1 st x / s C 2 nd y 0 N N = 2 nd y / j 1 st y / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
573 562 572 sylib x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
574 phpreu 0 N Fin 0 N 0 N i 0 N j 0 N i = 1 st x / s C i 0 N ∃! j 0 N i = 1 st x / s C
575 23 464 574 mp2an i 0 N j 0 N i = 1 st x / s C i 0 N ∃! j 0 N i = 1 st x / s C
576 reurmo ∃! j 0 N i = 1 st x / s C * j 0 N i = 1 st x / s C
577 576 ralimi i 0 N ∃! j 0 N i = 1 st x / s C i 0 N * j 0 N i = 1 st x / s C
578 575 577 sylbi i 0 N j 0 N i = 1 st x / s C i 0 N * j 0 N i = 1 st x / s C
579 eqeq1 i = N i = 1 st x / s C N = 1 st x / s C
580 579 rmobidv i = N * j 0 N i = 1 st x / s C * j 0 N N = 1 st x / s C
581 580 rspcva N 0 N i 0 N * j 0 N i = 1 st x / s C * j 0 N N = 1 st x / s C
582 232 578 581 syl2an φ i 0 N j 0 N i = 1 st x / s C * j 0 N N = 1 st x / s C
583 nfv k N = 1 st x / s C
584 583 rmo3 * j 0 N N = 1 st x / s C j 0 N k 0 N N = 1 st x / s C k j N = 1 st x / s C j = k
585 582 584 sylib φ i 0 N j 0 N i = 1 st x / s C j 0 N k 0 N N = 1 st x / s C k j N = 1 st x / s C j = k
586 nfcsb1v _ j 2 nd x / j 1 st x / s C
587 586 nfeq2 j N = 2 nd x / j 1 st x / s C
588 nfs1v j k j N = 1 st x / s C
589 587 588 nfan j N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C
590 nfv j 2 nd x = k
591 589 590 nfim j N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C 2 nd x = k
592 nfv k N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y
593 csbeq1a j = 2 nd x 1 st x / s C = 2 nd x / j 1 st x / s C
594 593 eqeq2d j = 2 nd x N = 1 st x / s C N = 2 nd x / j 1 st x / s C
595 594 anbi1d j = 2 nd x N = 1 st x / s C k j N = 1 st x / s C N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C
596 eqeq1 j = 2 nd x j = k 2 nd x = k
597 595 596 imbi12d j = 2 nd x N = 1 st x / s C k j N = 1 st x / s C j = k N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C 2 nd x = k
598 sbsbc k j N = 1 st x / s C [˙k / j]˙ N = 1 st x / s C
599 vex k V
600 sbceq2g k V [˙k / j]˙ N = 1 st x / s C N = k / j 1 st x / s C
601 599 600 ax-mp [˙k / j]˙ N = 1 st x / s C N = k / j 1 st x / s C
602 598 601 bitri k j N = 1 st x / s C N = k / j 1 st x / s C
603 csbeq1 k = 2 nd y k / j 1 st x / s C = 2 nd y / j 1 st x / s C
604 603 eqeq2d k = 2 nd y N = k / j 1 st x / s C N = 2 nd y / j 1 st x / s C
605 602 604 syl5bb k = 2 nd y k j N = 1 st x / s C N = 2 nd y / j 1 st x / s C
606 605 anbi2d k = 2 nd y N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C
607 eqeq2 k = 2 nd y 2 nd x = k 2 nd x = 2 nd y
608 606 607 imbi12d k = 2 nd y N = 2 nd x / j 1 st x / s C k j N = 1 st x / s C 2 nd x = k N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y
609 591 592 597 608 rspc2 2 nd x 0 N 2 nd y 0 N j 0 N k 0 N N = 1 st x / s C k j N = 1 st x / s C j = k N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y
610 585 609 syl5com φ i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y
611 610 impr φ i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y
612 csbeq1 1 st x = 1 st y 1 st x / s C = 1 st y / s C
613 612 csbeq2dv 1 st x = 1 st y 2 nd y / j 1 st x / s C = 2 nd y / j 1 st y / s C
614 613 eqeq2d 1 st x = 1 st y N = 2 nd y / j 1 st x / s C N = 2 nd y / j 1 st y / s C
615 614 anbi2d 1 st x = 1 st y N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C
616 615 imbi1d 1 st x = 1 st y N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st x / s C 2 nd x = 2 nd y N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C 2 nd x = 2 nd y
617 611 616 syl5ibcom φ i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N 1 st x = 1 st y N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C 2 nd x = 2 nd y
618 617 com23 φ i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C 1 st x = 1 st y 2 nd x = 2 nd y
619 618 impr φ i 0 N j 0 N i = 1 st x / s C 2 nd x 0 N 2 nd y 0 N N = 2 nd x / j 1 st x / s C N = 2 nd y / j 1 st y / s C 1 st x = 1 st y 2 nd x = 2 nd y
620 573 619 sylan2 φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = 1 st y 2 nd x = 2 nd y
621 elrabi x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
622 elrabi y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N
623 xpopth x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x = 1 st y 2 nd x = 2 nd y x = y
624 623 biimpd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x = 1 st y 2 nd x = 2 nd y x = y
625 624 expd x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N y 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N 1 st x = 1 st y 2 nd x = 2 nd y x = y
626 621 622 625 syl2an x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = 1 st y 2 nd x = 2 nd y x = y
627 626 adantl φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = 1 st y 2 nd x = 2 nd y x = y
628 620 627 mpdd φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st x = 1 st y x = y
629 541 628 sylbid φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y x = y
630 629 ralrimivva φ x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y x = y
631 dff13 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C x t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C x = 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C y x = y
632 537 630 631 sylanbrc φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
633 df-f1o 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
634 632 535 633 sylanbrc φ 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
635 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C Fin
636 138 635 ax-mp t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C Fin
637 636 elexi t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C V
638 637 f1oen 1 st t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C : t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C 1-1 onto s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
639 634 638 syl φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
640 rabfi 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N Fin s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C Fin
641 136 640 ax-mp s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C Fin
642 hashen t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C Fin s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C Fin t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
643 636 641 642 mp2an t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
644 639 643 sylibr φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
645 644 oveq2d φ t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | N = 2 nd t / j 1 st t / s C i 0 N j 0 N i = 1 st t / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
646 202 425 645 3eqtr3d φ x 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N x × y 0 N | i 0 N 1 j 0 N y i = x / s C j 0 N N x / s C = t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C
647 135 646 breqtrd φ 2 t 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N × 0 N | i 0 N 1 j 0 N 2 nd t i = 1 st t / s C s 0 ..^ K 1 N × f | f : 1 N 1-1 onto 1 N | i 0 N j 0 N i = C