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 
|- ( ph -> N e. NN )
poimirlem4.1 
|- ( ph -> K e. NN )
poimirlem4.2 
|- ( ph -> M e. NN0 )
poimirlem4.3 
|- ( ph -> M < N )
poimirlem3.4 
|- ( ph -> T : ( 1 ... M ) --> ( 0 ..^ K ) )
poimirlem3.5 
|- ( ph -> U : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
Assertion poimirlem3 
|- ( ph -> ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... M ) ) X. { 0 } ) ) ) u. ( ( ( M + 1 ) ... N ) X. { 0 } ) ) / p ]_ B -> ( <. ( T u. { <. ( M + 1 ) , 0 >. } ) , ( U u. { <. ( M + 1 ) , ( M + 1 ) >. } ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... ( M + 1 ) ) ) X. { f | f : ( 1 ... ( M + 1 ) ) -1-1-onto-> ( 1 ... ( M + 1 ) ) } ) /\ ( A. i e. ( 0 ... M ) E. j e. ( 0 ... M ) i = [_ ( ( ( T u. { <. ( M + 1 ) , 0 >. } ) oF + ( ( ( ( U u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( U u. { <. ( M + 1 ) , ( M + 1 ) >. } ) " ( ( j + 1 ) ... ( M + 1 ) ) ) X. { 0 } ) ) ) u. ( ( ( ( M + 1 ) + 1 ) ... N ) X. { 0 } ) ) / p ]_ B /\ ( ( T u. { <. ( M + 1 ) , 0 >. } ) ` ( M + 1 ) ) = 0 /\ ( ( U u. { <. ( M + 1 ) , ( M + 1 ) >. } ) ` ( M + 1 ) ) = ( M + 1 ) ) ) ) )

Proof

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