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