Metamath Proof Explorer


Theorem poimirlem3

Description: Lemma for poimir to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 φ N
poimirlem4.1 φ K
poimirlem4.2 φ M 0
poimirlem4.3 φ M < N
poimirlem3.4 φ T : 1 M 0 ..^ K
poimirlem3.5 φ U : 1 M 1-1 onto 1 M
Assertion poimirlem3 φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B T M + 1 0 U M + 1 M + 1 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1

Proof

Step Hyp Ref Expression
1 poimir.0 φ N
2 poimirlem4.1 φ K
3 poimirlem4.2 φ M 0
4 poimirlem4.3 φ M < N
5 poimirlem3.4 φ T : 1 M 0 ..^ K
6 poimirlem3.5 φ U : 1 M 1-1 onto 1 M
7 5 ffnd φ T Fn 1 M
8 7 adantr φ j 0 M T Fn 1 M
9 1ex 1 V
10 fnconstg 1 V U 1 j × 1 Fn U 1 j
11 9 10 ax-mp U 1 j × 1 Fn U 1 j
12 c0ex 0 V
13 fnconstg 0 V U j + 1 M × 0 Fn U j + 1 M
14 12 13 ax-mp U j + 1 M × 0 Fn U j + 1 M
15 11 14 pm3.2i U 1 j × 1 Fn U 1 j U j + 1 M × 0 Fn U j + 1 M
16 dff1o3 U : 1 M 1-1 onto 1 M U : 1 M onto 1 M Fun U -1
17 16 simprbi U : 1 M 1-1 onto 1 M Fun U -1
18 imain Fun U -1 U 1 j j + 1 M = U 1 j U j + 1 M
19 6 17 18 3syl φ U 1 j j + 1 M = U 1 j U j + 1 M
20 elfznn0 j 0 M j 0
21 20 nn0red j 0 M j
22 21 ltp1d j 0 M j < j + 1
23 fzdisj j < j + 1 1 j j + 1 M =
24 22 23 syl j 0 M 1 j j + 1 M =
25 24 imaeq2d j 0 M U 1 j j + 1 M = U
26 ima0 U =
27 25 26 eqtrdi j 0 M U 1 j j + 1 M =
28 19 27 sylan9req φ j 0 M U 1 j U j + 1 M =
29 fnun U 1 j × 1 Fn U 1 j U j + 1 M × 0 Fn U j + 1 M U 1 j U j + 1 M = U 1 j × 1 U j + 1 M × 0 Fn U 1 j U j + 1 M
30 15 28 29 sylancr φ j 0 M U 1 j × 1 U j + 1 M × 0 Fn U 1 j U j + 1 M
31 imaundi U 1 j j + 1 M = U 1 j U j + 1 M
32 nn0p1nn j 0 j + 1
33 nnuz = 1
34 32 33 eleqtrdi j 0 j + 1 1
35 20 34 syl j 0 M j + 1 1
36 elfzuz3 j 0 M M j
37 fzsplit2 j + 1 1 M j 1 M = 1 j j + 1 M
38 35 36 37 syl2anc j 0 M 1 M = 1 j j + 1 M
39 38 eqcomd j 0 M 1 j j + 1 M = 1 M
40 39 imaeq2d j 0 M U 1 j j + 1 M = U 1 M
41 f1ofo U : 1 M 1-1 onto 1 M U : 1 M onto 1 M
42 foima U : 1 M onto 1 M U 1 M = 1 M
43 6 41 42 3syl φ U 1 M = 1 M
44 40 43 sylan9eqr φ j 0 M U 1 j j + 1 M = 1 M
45 31 44 eqtr3id φ j 0 M U 1 j U j + 1 M = 1 M
46 45 fneq2d φ j 0 M U 1 j × 1 U j + 1 M × 0 Fn U 1 j U j + 1 M U 1 j × 1 U j + 1 M × 0 Fn 1 M
47 30 46 mpbid φ j 0 M U 1 j × 1 U j + 1 M × 0 Fn 1 M
48 ovexd φ j 0 M 1 M V
49 inidm 1 M 1 M = 1 M
50 eqidd φ j 0 M n 1 M T n = T n
51 eqidd φ j 0 M n 1 M U 1 j × 1 U j + 1 M × 0 n = U 1 j × 1 U j + 1 M × 0 n
52 8 47 48 48 49 50 51 offval φ j 0 M T + f U 1 j × 1 U j + 1 M × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n
53 nn0p1nn M 0 M + 1
54 3 53 syl φ M + 1
55 54 nnzd φ M + 1
56 uzid M + 1 M + 1 M + 1
57 peano2uz M + 1 M + 1 M + 1 + 1 M + 1
58 55 56 57 3syl φ M + 1 + 1 M + 1
59 3 nn0zd φ M
60 1 nnzd φ N
61 zltp1le M N M < N M + 1 N
62 peano2z M M + 1
63 eluz M + 1 N N M + 1 M + 1 N
64 62 63 sylan M N N M + 1 M + 1 N
65 61 64 bitr4d M N M < N N M + 1
66 59 60 65 syl2anc φ M < N N M + 1
67 4 66 mpbid φ N M + 1
68 fzsplit2 M + 1 + 1 M + 1 N M + 1 M + 1 N = M + 1 M + 1 M + 1 + 1 N
69 58 67 68 syl2anc φ M + 1 N = M + 1 M + 1 M + 1 + 1 N
70 fzsn M + 1 M + 1 M + 1 = M + 1
71 55 70 syl φ M + 1 M + 1 = M + 1
72 71 uneq1d φ M + 1 M + 1 M + 1 + 1 N = M + 1 M + 1 + 1 N
73 69 72 eqtrd φ M + 1 N = M + 1 M + 1 + 1 N
74 73 xpeq1d φ M + 1 N × 0 = M + 1 M + 1 + 1 N × 0
75 xpundir M + 1 M + 1 + 1 N × 0 = M + 1 × 0 M + 1 + 1 N × 0
76 ovex M + 1 V
77 76 12 xpsn M + 1 × 0 = M + 1 0
78 77 uneq1i M + 1 × 0 M + 1 + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
79 75 78 eqtri M + 1 M + 1 + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
80 74 79 eqtrdi φ M + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
81 80 adantr φ j 0 M M + 1 N × 0 = M + 1 0 M + 1 + 1 N × 0
82 52 81 uneq12d φ j 0 M T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0 M + 1 + 1 N × 0
83 unass n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0 M + 1 + 1 N × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0 M + 1 + 1 N × 0
84 82 83 eqtr4di φ j 0 M T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0 M + 1 + 1 N × 0
85 3 nn0red φ M
86 85 ltp1d φ M < M + 1
87 54 nnred φ M + 1
88 85 87 ltnled φ M < M + 1 ¬ M + 1 M
89 86 88 mpbid φ ¬ M + 1 M
90 elfzle2 M + 1 1 M M + 1 M
91 89 90 nsyl φ ¬ M + 1 1 M
92 disjsn 1 M M + 1 = ¬ M + 1 1 M
93 91 92 sylibr φ 1 M M + 1 =
94 eqid M + 1 0 = M + 1 0
95 76 12 fsn M + 1 0 : M + 1 0 M + 1 0 = M + 1 0
96 94 95 mpbir M + 1 0 : M + 1 0
97 fun T : 1 M 0 ..^ K M + 1 0 : M + 1 0 1 M M + 1 = T M + 1 0 : 1 M M + 1 0 ..^ K 0
98 96 97 mpanl2 T : 1 M 0 ..^ K 1 M M + 1 = T M + 1 0 : 1 M M + 1 0 ..^ K 0
99 5 93 98 syl2anc φ T M + 1 0 : 1 M M + 1 0 ..^ K 0
100 1z 1
101 nn0uz 0 = 0
102 1m1e0 1 1 = 0
103 102 fveq2i 1 1 = 0
104 101 103 eqtr4i 0 = 1 1
105 3 104 eleqtrdi φ M 1 1
106 fzsuc2 1 M 1 1 1 M + 1 = 1 M M + 1
107 100 105 106 sylancr φ 1 M + 1 = 1 M M + 1
108 107 eqcomd φ 1 M M + 1 = 1 M + 1
109 lbfzo0 0 0 ..^ K K
110 2 109 sylibr φ 0 0 ..^ K
111 110 snssd φ 0 0 ..^ K
112 ssequn2 0 0 ..^ K 0 ..^ K 0 = 0 ..^ K
113 111 112 sylib φ 0 ..^ K 0 = 0 ..^ K
114 108 113 feq23d φ T M + 1 0 : 1 M M + 1 0 ..^ K 0 T M + 1 0 : 1 M + 1 0 ..^ K
115 99 114 mpbid φ T M + 1 0 : 1 M + 1 0 ..^ K
116 115 ffnd φ T M + 1 0 Fn 1 M + 1
117 116 adantr φ j 0 M T M + 1 0 Fn 1 M + 1
118 fnconstg 1 V U M + 1 M + 1 1 j × 1 Fn U M + 1 M + 1 1 j
119 9 118 ax-mp U M + 1 M + 1 1 j × 1 Fn U M + 1 M + 1 1 j
120 fnconstg 0 V U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 j + 1 M + 1
121 12 120 ax-mp U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 j + 1 M + 1
122 119 121 pm3.2i U M + 1 M + 1 1 j × 1 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 j + 1 M + 1
123 76 76 f1osn M + 1 M + 1 : M + 1 1-1 onto M + 1
124 f1oun U : 1 M 1-1 onto 1 M M + 1 M + 1 : M + 1 1-1 onto M + 1 1 M M + 1 = 1 M M + 1 = U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
125 123 124 mpanl2 U : 1 M 1-1 onto 1 M 1 M M + 1 = 1 M M + 1 = U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
126 6 93 93 125 syl12anc φ U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
127 dff1o3 U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1 U M + 1 M + 1 : 1 M M + 1 onto 1 M M + 1 Fun U M + 1 M + 1 -1
128 127 simprbi U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1 Fun U M + 1 M + 1 -1
129 imain Fun U M + 1 M + 1 -1 U M + 1 M + 1 1 j j + 1 M + 1 = U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
130 126 128 129 3syl φ U M + 1 M + 1 1 j j + 1 M + 1 = U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
131 fzdisj j < j + 1 1 j j + 1 M + 1 =
132 22 131 syl j 0 M 1 j j + 1 M + 1 =
133 132 imaeq2d j 0 M U M + 1 M + 1 1 j j + 1 M + 1 = U M + 1 M + 1
134 ima0 U M + 1 M + 1 =
135 133 134 eqtrdi j 0 M U M + 1 M + 1 1 j j + 1 M + 1 =
136 130 135 sylan9req φ j 0 M U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 =
137 fnun U M + 1 M + 1 1 j × 1 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 j + 1 M + 1 U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 = U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
138 122 136 137 sylancr φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
139 f1ofo U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1 U M + 1 M + 1 : 1 M M + 1 onto 1 M M + 1
140 foima U M + 1 M + 1 : 1 M M + 1 onto 1 M M + 1 U M + 1 M + 1 1 M M + 1 = 1 M M + 1
141 126 139 140 3syl φ U M + 1 M + 1 1 M M + 1 = 1 M M + 1
142 107 imaeq2d φ U M + 1 M + 1 1 M + 1 = U M + 1 M + 1 1 M M + 1
143 141 142 107 3eqtr4d φ U M + 1 M + 1 1 M + 1 = 1 M + 1
144 peano2uz M j M + 1 j
145 36 144 syl j 0 M M + 1 j
146 fzsplit2 j + 1 1 M + 1 j 1 M + 1 = 1 j j + 1 M + 1
147 35 145 146 syl2anc j 0 M 1 M + 1 = 1 j j + 1 M + 1
148 147 imaeq2d j 0 M U M + 1 M + 1 1 M + 1 = U M + 1 M + 1 1 j j + 1 M + 1
149 143 148 sylan9req φ j 0 M 1 M + 1 = U M + 1 M + 1 1 j j + 1 M + 1
150 imaundi U M + 1 M + 1 1 j j + 1 M + 1 = U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
151 149 150 eqtrdi φ j 0 M 1 M + 1 = U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
152 151 fneq2d φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 Fn 1 M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1
153 138 152 mpbird φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 Fn 1 M + 1
154 ovexd φ j 0 M 1 M + 1 V
155 inidm 1 M + 1 1 M + 1 = 1 M + 1
156 eqidd φ j 0 M n 1 M + 1 T M + 1 0 n = T M + 1 0 n
157 eqidd φ j 0 M n 1 M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n
158 117 153 154 154 155 156 157 offval φ j 0 M T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 = n 1 M + 1 T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n
159 imadmrn M + 1 × M + 1 dom M + 1 × M + 1 = ran M + 1 × M + 1
160 76 76 xpsn M + 1 × M + 1 = M + 1 M + 1
161 160 imaeq1i M + 1 × M + 1 dom M + 1 × M + 1 = M + 1 M + 1 dom M + 1 × M + 1
162 dmxpid dom M + 1 × M + 1 = M + 1
163 162 imaeq2i M + 1 M + 1 dom M + 1 × M + 1 = M + 1 M + 1 M + 1
164 161 163 eqtri M + 1 × M + 1 dom M + 1 × M + 1 = M + 1 M + 1 M + 1
165 rnxpid ran M + 1 × M + 1 = M + 1
166 159 164 165 3eqtr3ri M + 1 = M + 1 M + 1 M + 1
167 eluzp1p1 M j M + 1 j + 1
168 eluzfz2 M + 1 j + 1 M + 1 j + 1 M + 1
169 36 167 168 3syl j 0 M M + 1 j + 1 M + 1
170 169 snssd j 0 M M + 1 j + 1 M + 1
171 imass2 M + 1 j + 1 M + 1 M + 1 M + 1 M + 1 M + 1 M + 1 j + 1 M + 1
172 170 171 syl j 0 M M + 1 M + 1 M + 1 M + 1 M + 1 j + 1 M + 1
173 166 172 eqsstrid j 0 M M + 1 M + 1 M + 1 j + 1 M + 1
174 76 snid M + 1 M + 1
175 ssel M + 1 M + 1 M + 1 j + 1 M + 1 M + 1 M + 1 M + 1 M + 1 M + 1 j + 1 M + 1
176 173 174 175 mpisyl j 0 M M + 1 M + 1 M + 1 j + 1 M + 1
177 elun2 M + 1 M + 1 M + 1 j + 1 M + 1 M + 1 U j + 1 M + 1 M + 1 M + 1 j + 1 M + 1
178 176 177 syl j 0 M M + 1 U j + 1 M + 1 M + 1 M + 1 j + 1 M + 1
179 imaundir U M + 1 M + 1 j + 1 M + 1 = U j + 1 M + 1 M + 1 M + 1 j + 1 M + 1
180 178 179 eleqtrrdi j 0 M M + 1 U M + 1 M + 1 j + 1 M + 1
181 180 adantl φ j 0 M M + 1 U M + 1 M + 1 j + 1 M + 1
182 12 a1i φ j 0 M 0 V
183 108 adantr φ j 0 M 1 M M + 1 = 1 M + 1
184 fveq2 n = M + 1 T M + 1 0 n = T M + 1 0 M + 1
185 76 12 fnsn M + 1 0 Fn M + 1
186 fvun2 T Fn 1 M M + 1 0 Fn M + 1 1 M M + 1 = M + 1 M + 1 T M + 1 0 M + 1 = M + 1 0 M + 1
187 185 186 mp3an2 T Fn 1 M 1 M M + 1 = M + 1 M + 1 T M + 1 0 M + 1 = M + 1 0 M + 1
188 174 187 mpanr2 T Fn 1 M 1 M M + 1 = T M + 1 0 M + 1 = M + 1 0 M + 1
189 7 93 188 syl2anc φ T M + 1 0 M + 1 = M + 1 0 M + 1
190 76 12 fvsn M + 1 0 M + 1 = 0
191 189 190 eqtrdi φ T M + 1 0 M + 1 = 0
192 184 191 sylan9eqr φ n = M + 1 T M + 1 0 n = 0
193 192 adantlr φ j 0 M n = M + 1 T M + 1 0 n = 0
194 fveq2 n = M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1
195 fvun2 U M + 1 M + 1 1 j × 1 Fn U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 × 0 Fn U M + 1 M + 1 j + 1 M + 1 U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 = M + 1 U M + 1 M + 1 j + 1 M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = U M + 1 M + 1 j + 1 M + 1 × 0 M + 1
196 119 121 195 mp3an12 U M + 1 M + 1 1 j U M + 1 M + 1 j + 1 M + 1 = M + 1 U M + 1 M + 1 j + 1 M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = U M + 1 M + 1 j + 1 M + 1 × 0 M + 1
197 136 181 196 syl2anc φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = U M + 1 M + 1 j + 1 M + 1 × 0 M + 1
198 12 fvconst2 M + 1 U M + 1 M + 1 j + 1 M + 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = 0
199 180 198 syl j 0 M U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = 0
200 199 adantl φ j 0 M U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = 0
201 197 200 eqtrd φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 = 0
202 194 201 sylan9eqr φ j 0 M n = M + 1 U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = 0
203 193 202 oveq12d φ j 0 M n = M + 1 T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = 0 + 0
204 00id 0 + 0 = 0
205 203 204 eqtrdi φ j 0 M n = M + 1 T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = 0
206 181 182 183 205 fmptapd φ j 0 M n 1 M T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n M + 1 0 = n 1 M + 1 T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n
207 7 93 jca φ T Fn 1 M 1 M M + 1 =
208 fvun1 T Fn 1 M M + 1 0 Fn M + 1 1 M M + 1 = n 1 M T M + 1 0 n = T n
209 185 208 mp3an2 T Fn 1 M 1 M M + 1 = n 1 M T M + 1 0 n = T n
210 209 anassrs T Fn 1 M 1 M M + 1 = n 1 M T M + 1 0 n = T n
211 207 210 sylan φ n 1 M T M + 1 0 n = T n
212 211 adantlr φ j 0 M n 1 M T M + 1 0 n = T n
213 fvres n 1 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 1 M n = U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n
214 213 eqcomd n 1 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 1 M n
215 resundir U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 1 M = U M + 1 M + 1 1 j × 1 1 M U M + 1 M + 1 j + 1 M + 1 × 0 1 M
216 relxp Rel U 1 j × 1
217 dmxpss dom U 1 j × 1 U 1 j
218 imassrn U 1 j ran U
219 217 218 sstri dom U 1 j × 1 ran U
220 f1of U : 1 M 1-1 onto 1 M U : 1 M 1 M
221 frn U : 1 M 1 M ran U 1 M
222 6 220 221 3syl φ ran U 1 M
223 219 222 sstrid φ dom U 1 j × 1 1 M
224 relssres Rel U 1 j × 1 dom U 1 j × 1 1 M U 1 j × 1 1 M = U 1 j × 1
225 216 223 224 sylancr φ U 1 j × 1 1 M = U 1 j × 1
226 225 adantr φ j 0 M U 1 j × 1 1 M = U 1 j × 1
227 imassrn M + 1 M + 1 1 j ran M + 1 M + 1
228 76 rnsnop ran M + 1 M + 1 = M + 1
229 227 228 sseqtri M + 1 M + 1 1 j M + 1
230 ssrin M + 1 M + 1 1 j M + 1 M + 1 M + 1 1 j 1 M M + 1 1 M
231 229 230 ax-mp M + 1 M + 1 1 j 1 M M + 1 1 M
232 incom M + 1 1 M = 1 M M + 1
233 232 93 syl5eq φ M + 1 1 M =
234 231 233 sseqtrid φ M + 1 M + 1 1 j 1 M
235 ss0 M + 1 M + 1 1 j 1 M M + 1 M + 1 1 j 1 M =
236 234 235 syl φ M + 1 M + 1 1 j 1 M =
237 fnconstg 1 V M + 1 M + 1 1 j × 1 Fn M + 1 M + 1 1 j
238 fnresdisj M + 1 M + 1 1 j × 1 Fn M + 1 M + 1 1 j M + 1 M + 1 1 j 1 M = M + 1 M + 1 1 j × 1 1 M =
239 9 237 238 mp2b M + 1 M + 1 1 j 1 M = M + 1 M + 1 1 j × 1 1 M =
240 236 239 sylib φ M + 1 M + 1 1 j × 1 1 M =
241 240 adantr φ j 0 M M + 1 M + 1 1 j × 1 1 M =
242 226 241 uneq12d φ j 0 M U 1 j × 1 1 M M + 1 M + 1 1 j × 1 1 M = U 1 j × 1
243 imaundir U M + 1 M + 1 1 j = U 1 j M + 1 M + 1 1 j
244 243 xpeq1i U M + 1 M + 1 1 j × 1 = U 1 j M + 1 M + 1 1 j × 1
245 xpundir U 1 j M + 1 M + 1 1 j × 1 = U 1 j × 1 M + 1 M + 1 1 j × 1
246 244 245 eqtri U M + 1 M + 1 1 j × 1 = U 1 j × 1 M + 1 M + 1 1 j × 1
247 246 reseq1i U M + 1 M + 1 1 j × 1 1 M = U 1 j × 1 M + 1 M + 1 1 j × 1 1 M
248 resundir U 1 j × 1 M + 1 M + 1 1 j × 1 1 M = U 1 j × 1 1 M M + 1 M + 1 1 j × 1 1 M
249 247 248 eqtr2i U 1 j × 1 1 M M + 1 M + 1 1 j × 1 1 M = U M + 1 M + 1 1 j × 1 1 M
250 un0 U 1 j × 1 = U 1 j × 1
251 242 249 250 3eqtr3g φ j 0 M U M + 1 M + 1 1 j × 1 1 M = U 1 j × 1
252 f1odm U : 1 M 1-1 onto 1 M dom U = 1 M
253 6 252 syl φ dom U = 1 M
254 253 ineq2d φ j + 1 M + 1 dom U = j + 1 M + 1 1 M
255 254 reseq2d φ U j + 1 M + 1 dom U = U j + 1 M + 1 1 M
256 f1orel U : 1 M 1-1 onto 1 M Rel U
257 resindm Rel U U j + 1 M + 1 dom U = U j + 1 M + 1
258 6 256 257 3syl φ U j + 1 M + 1 dom U = U j + 1 M + 1
259 255 258 eqtr3d φ U j + 1 M + 1 1 M = U j + 1 M + 1
260 38 ineq2d j 0 M j + 1 M + 1 1 M = j + 1 M + 1 1 j j + 1 M
261 fzssp1 j + 1 M j + 1 M + 1
262 sseqin2 j + 1 M j + 1 M + 1 j + 1 M + 1 j + 1 M = j + 1 M
263 261 262 mpbi j + 1 M + 1 j + 1 M = j + 1 M
264 263 a1i j 0 M j + 1 M + 1 j + 1 M = j + 1 M
265 incom j + 1 M + 1 1 j = 1 j j + 1 M + 1
266 265 132 syl5eq j 0 M j + 1 M + 1 1 j =
267 264 266 uneq12d j 0 M j + 1 M + 1 j + 1 M j + 1 M + 1 1 j = j + 1 M
268 uncom j + 1 M + 1 j + 1 M j + 1 M + 1 1 j = j + 1 M + 1 1 j j + 1 M + 1 j + 1 M
269 indi j + 1 M + 1 1 j j + 1 M = j + 1 M + 1 1 j j + 1 M + 1 j + 1 M
270 268 269 eqtr4i j + 1 M + 1 j + 1 M j + 1 M + 1 1 j = j + 1 M + 1 1 j j + 1 M
271 un0 j + 1 M = j + 1 M
272 267 270 271 3eqtr3g j 0 M j + 1 M + 1 1 j j + 1 M = j + 1 M
273 260 272 eqtrd j 0 M j + 1 M + 1 1 M = j + 1 M
274 273 reseq2d j 0 M U j + 1 M + 1 1 M = U j + 1 M
275 259 274 sylan9req φ j 0 M U j + 1 M + 1 = U j + 1 M
276 275 rneqd φ j 0 M ran U j + 1 M + 1 = ran U j + 1 M
277 df-ima U j + 1 M + 1 = ran U j + 1 M + 1
278 df-ima U j + 1 M = ran U j + 1 M
279 276 277 278 3eqtr4g φ j 0 M U j + 1 M + 1 = U j + 1 M
280 279 xpeq1d φ j 0 M U j + 1 M + 1 × 0 = U j + 1 M × 0
281 280 reseq1d φ j 0 M U j + 1 M + 1 × 0 1 M = U j + 1 M × 0 1 M
282 relxp Rel U j + 1 M × 0
283 dmxpss dom U j + 1 M × 0 U j + 1 M
284 imassrn U j + 1 M ran U
285 283 284 sstri dom U j + 1 M × 0 ran U
286 285 222 sstrid φ dom U j + 1 M × 0 1 M
287 relssres Rel U j + 1 M × 0 dom U j + 1 M × 0 1 M U j + 1 M × 0 1 M = U j + 1 M × 0
288 282 286 287 sylancr φ U j + 1 M × 0 1 M = U j + 1 M × 0
289 288 adantr φ j 0 M U j + 1 M × 0 1 M = U j + 1 M × 0
290 281 289 eqtrd φ j 0 M U j + 1 M + 1 × 0 1 M = U j + 1 M × 0
291 imassrn M + 1 M + 1 j + 1 M + 1 ran M + 1 M + 1
292 291 228 sseqtri M + 1 M + 1 j + 1 M + 1 M + 1
293 ssrin M + 1 M + 1 j + 1 M + 1 M + 1 M + 1 M + 1 j + 1 M + 1 1 M M + 1 1 M
294 292 293 ax-mp M + 1 M + 1 j + 1 M + 1 1 M M + 1 1 M
295 294 233 sseqtrid φ M + 1 M + 1 j + 1 M + 1 1 M
296 ss0 M + 1 M + 1 j + 1 M + 1 1 M M + 1 M + 1 j + 1 M + 1 1 M =
297 295 296 syl φ M + 1 M + 1 j + 1 M + 1 1 M =
298 fnconstg 0 V M + 1 M + 1 j + 1 M + 1 × 0 Fn M + 1 M + 1 j + 1 M + 1
299 fnresdisj M + 1 M + 1 j + 1 M + 1 × 0 Fn M + 1 M + 1 j + 1 M + 1 M + 1 M + 1 j + 1 M + 1 1 M = M + 1 M + 1 j + 1 M + 1 × 0 1 M =
300 12 298 299 mp2b M + 1 M + 1 j + 1 M + 1 1 M = M + 1 M + 1 j + 1 M + 1 × 0 1 M =
301 297 300 sylib φ M + 1 M + 1 j + 1 M + 1 × 0 1 M =
302 301 adantr φ j 0 M M + 1 M + 1 j + 1 M + 1 × 0 1 M =
303 290 302 uneq12d φ j 0 M U j + 1 M + 1 × 0 1 M M + 1 M + 1 j + 1 M + 1 × 0 1 M = U j + 1 M × 0
304 179 xpeq1i U M + 1 M + 1 j + 1 M + 1 × 0 = U j + 1 M + 1 M + 1 M + 1 j + 1 M + 1 × 0
305 xpundir U j + 1 M + 1 M + 1 M + 1 j + 1 M + 1 × 0 = U j + 1 M + 1 × 0 M + 1 M + 1 j + 1 M + 1 × 0
306 304 305 eqtri U M + 1 M + 1 j + 1 M + 1 × 0 = U j + 1 M + 1 × 0 M + 1 M + 1 j + 1 M + 1 × 0
307 306 reseq1i U M + 1 M + 1 j + 1 M + 1 × 0 1 M = U j + 1 M + 1 × 0 M + 1 M + 1 j + 1 M + 1 × 0 1 M
308 resundir U j + 1 M + 1 × 0 M + 1 M + 1 j + 1 M + 1 × 0 1 M = U j + 1 M + 1 × 0 1 M M + 1 M + 1 j + 1 M + 1 × 0 1 M
309 307 308 eqtr2i U j + 1 M + 1 × 0 1 M M + 1 M + 1 j + 1 M + 1 × 0 1 M = U M + 1 M + 1 j + 1 M + 1 × 0 1 M
310 un0 U j + 1 M × 0 = U j + 1 M × 0
311 303 309 310 3eqtr3g φ j 0 M U M + 1 M + 1 j + 1 M + 1 × 0 1 M = U j + 1 M × 0
312 251 311 uneq12d φ j 0 M U M + 1 M + 1 1 j × 1 1 M U M + 1 M + 1 j + 1 M + 1 × 0 1 M = U 1 j × 1 U j + 1 M × 0
313 215 312 syl5eq φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 1 M = U 1 j × 1 U j + 1 M × 0
314 313 fveq1d φ j 0 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 1 M n = U 1 j × 1 U j + 1 M × 0 n
315 214 314 sylan9eqr φ j 0 M n 1 M U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = U 1 j × 1 U j + 1 M × 0 n
316 212 315 oveq12d φ j 0 M n 1 M T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = T n + U 1 j × 1 U j + 1 M × 0 n
317 316 mpteq2dva φ j 0 M n 1 M T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n
318 317 uneq1d φ j 0 M n 1 M T M + 1 0 n + U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 n M + 1 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0
319 158 206 318 3eqtr2d φ j 0 M T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0
320 319 uneq1d φ j 0 M T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 = n 1 M T n + U 1 j × 1 U j + 1 M × 0 n M + 1 0 M + 1 + 1 N × 0
321 84 320 eqtr4d φ j 0 M T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0
322 321 csbeq1d φ j 0 M T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
323 322 eqeq2d φ j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
324 323 rexbidva φ j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
325 324 ralbidv φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
326 325 biimpd φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B
327 f1ofn U : 1 M 1-1 onto 1 M U Fn 1 M
328 6 327 syl φ U Fn 1 M
329 76 76 fnsn M + 1 M + 1 Fn M + 1
330 fvun2 U Fn 1 M M + 1 M + 1 Fn M + 1 1 M M + 1 = M + 1 M + 1 U M + 1 M + 1 M + 1 = M + 1 M + 1 M + 1
331 329 330 mp3an2 U Fn 1 M 1 M M + 1 = M + 1 M + 1 U M + 1 M + 1 M + 1 = M + 1 M + 1 M + 1
332 174 331 mpanr2 U Fn 1 M 1 M M + 1 = U M + 1 M + 1 M + 1 = M + 1 M + 1 M + 1
333 328 93 332 syl2anc φ U M + 1 M + 1 M + 1 = M + 1 M + 1 M + 1
334 76 76 fvsn M + 1 M + 1 M + 1 = M + 1
335 333 334 eqtrdi φ U M + 1 M + 1 M + 1 = M + 1
336 191 335 jca φ T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1
337 326 336 jctird φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1
338 3anass i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1 i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1
339 337 338 syl6ibr φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1
340 5 96 jctir φ T : 1 M 0 ..^ K M + 1 0 : M + 1 0
341 340 93 97 syl2anc φ T M + 1 0 : 1 M M + 1 0 ..^ K 0
342 341 114 mpbid φ T M + 1 0 : 1 M + 1 0 ..^ K
343 ovex 0 ..^ K V
344 ovex 1 M + 1 V
345 343 344 elmap T M + 1 0 0 ..^ K 1 M + 1 T M + 1 0 : 1 M + 1 0 ..^ K
346 342 345 sylibr φ T M + 1 0 0 ..^ K 1 M + 1
347 ovex 1 M V
348 f1oexrnex U : 1 M 1-1 onto 1 M 1 M V U V
349 6 347 348 sylancl φ U V
350 snex M + 1 M + 1 V
351 unexg U V M + 1 M + 1 V U M + 1 M + 1 V
352 349 350 351 sylancl φ U M + 1 M + 1 V
353 f1oeq1 f = U M + 1 M + 1 f : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M + 1 1-1 onto 1 M + 1
354 353 elabg U M + 1 M + 1 V U M + 1 M + 1 f | f : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M + 1 1-1 onto 1 M + 1
355 352 354 syl φ U M + 1 M + 1 f | f : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M + 1 1-1 onto 1 M + 1
356 f1oeq23 1 M + 1 = 1 M M + 1 1 M + 1 = 1 M M + 1 U M + 1 M + 1 : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
357 107 107 356 syl2anc φ U M + 1 M + 1 : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
358 355 357 bitrd φ U M + 1 M + 1 f | f : 1 M + 1 1-1 onto 1 M + 1 U M + 1 M + 1 : 1 M M + 1 1-1 onto 1 M M + 1
359 126 358 mpbird φ U M + 1 M + 1 f | f : 1 M + 1 1-1 onto 1 M + 1
360 346 359 opelxpd φ T M + 1 0 U M + 1 M + 1 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1
361 339 360 jctild φ i 0 M j 0 M i = T + f U 1 j × 1 U j + 1 M × 0 M + 1 N × 0 / p B T M + 1 0 U M + 1 M + 1 0 ..^ K 1 M + 1 × f | f : 1 M + 1 1-1 onto 1 M + 1 i 0 M j 0 M i = T M + 1 0 + f U M + 1 M + 1 1 j × 1 U M + 1 M + 1 j + 1 M + 1 × 0 M + 1 + 1 N × 0 / p B T M + 1 0 M + 1 = 0 U M + 1 M + 1 M + 1 = M + 1