Metamath Proof Explorer

Theorem poimirlem2

Description: Lemma for poimir - consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem2.1 
|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
poimirlem2.2 
|- ( ph -> T : ( 1 ... N ) --> ZZ )
poimirlem2.3 
|- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem2.4 
|- ( ph -> V e. ( 1 ... ( N - 1 ) ) )
poimirlem2.5 
|- ( ph -> M e. ( ( 0 ... N ) \ { V } ) )
Assertion poimirlem2 
|- ( ph -> E* n e. ( 1 ... N ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem2.1 
 |-  ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
3 poimirlem2.2 
 |-  ( ph -> T : ( 1 ... N ) --> ZZ )
4 poimirlem2.3 
 |-  ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
5 poimirlem2.4 
 |-  ( ph -> V e. ( 1 ... ( N - 1 ) ) )
6 poimirlem2.5 
 |-  ( ph -> M e. ( ( 0 ... N ) \ { V } ) )
7 dff1o3 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
8 7 simprbi 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
9 4 8 syl 
 |-  ( ph -> Fun `' U )
10 imadif 
 |-  ( Fun `' U -> ( U " ( ( 1 ... N ) \ { ( V + 1 ) } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) )
11 9 10 syl 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { ( V + 1 ) } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) )
12 fzp1elp1 
 |-  ( V e. ( 1 ... ( N - 1 ) ) -> ( V + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
13 5 12 syl 
 |-  ( ph -> ( V + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
14 1 nncnd 
 |-  ( ph -> N e. CC )
15 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
16 14 15 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
17 16 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
18 13 17 eleqtrd 
 |-  ( ph -> ( V + 1 ) e. ( 1 ... N ) )
19 fzsplit 
 |-  ( ( V + 1 ) e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) )
20 18 19 syl 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) )
21 20 difeq1d 
 |-  ( ph -> ( ( 1 ... N ) \ { ( V + 1 ) } ) = ( ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) \ { ( V + 1 ) } ) )
22 difundir 
 |-  ( ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) \ { ( V + 1 ) } ) = ( ( ( 1 ... ( V + 1 ) ) \ { ( V + 1 ) } ) u. ( ( ( ( V + 1 ) + 1 ) ... N ) \ { ( V + 1 ) } ) )
23 elfzuz 
 |-  ( V e. ( 1 ... ( N - 1 ) ) -> V e. ( ZZ>= ` 1 ) )
24 5 23 syl 
 |-  ( ph -> V e. ( ZZ>= ` 1 ) )
25 fzsuc 
 |-  ( V e. ( ZZ>= ` 1 ) -> ( 1 ... ( V + 1 ) ) = ( ( 1 ... V ) u. { ( V + 1 ) } ) )
26 24 25 syl 
 |-  ( ph -> ( 1 ... ( V + 1 ) ) = ( ( 1 ... V ) u. { ( V + 1 ) } ) )
27 26 difeq1d 
 |-  ( ph -> ( ( 1 ... ( V + 1 ) ) \ { ( V + 1 ) } ) = ( ( ( 1 ... V ) u. { ( V + 1 ) } ) \ { ( V + 1 ) } ) )
28 difun2 
 |-  ( ( ( 1 ... V ) u. { ( V + 1 ) } ) \ { ( V + 1 ) } ) = ( ( 1 ... V ) \ { ( V + 1 ) } )
29 5 elfzelzd 
 |-  ( ph -> V e. ZZ )
30 29 zred 
 |-  ( ph -> V e. RR )
31 30 ltp1d 
 |-  ( ph -> V < ( V + 1 ) )
32 29 peano2zd 
 |-  ( ph -> ( V + 1 ) e. ZZ )
33 32 zred 
 |-  ( ph -> ( V + 1 ) e. RR )
34 30 33 ltnled 
 |-  ( ph -> ( V < ( V + 1 ) <-> -. ( V + 1 ) <_ V ) )
35 31 34 mpbid 
 |-  ( ph -> -. ( V + 1 ) <_ V )
36 elfzle2 
 |-  ( ( V + 1 ) e. ( 1 ... V ) -> ( V + 1 ) <_ V )
37 35 36 nsyl 
 |-  ( ph -> -. ( V + 1 ) e. ( 1 ... V ) )
38 difsn 
 |-  ( -. ( V + 1 ) e. ( 1 ... V ) -> ( ( 1 ... V ) \ { ( V + 1 ) } ) = ( 1 ... V ) )
39 37 38 syl 
 |-  ( ph -> ( ( 1 ... V ) \ { ( V + 1 ) } ) = ( 1 ... V ) )
40 28 39 eqtrid 
 |-  ( ph -> ( ( ( 1 ... V ) u. { ( V + 1 ) } ) \ { ( V + 1 ) } ) = ( 1 ... V ) )
41 27 40 eqtrd 
 |-  ( ph -> ( ( 1 ... ( V + 1 ) ) \ { ( V + 1 ) } ) = ( 1 ... V ) )
42 33 ltp1d 
 |-  ( ph -> ( V + 1 ) < ( ( V + 1 ) + 1 ) )
43 peano2re 
 |-  ( ( V + 1 ) e. RR -> ( ( V + 1 ) + 1 ) e. RR )
44 33 43 syl 
 |-  ( ph -> ( ( V + 1 ) + 1 ) e. RR )
45 33 44 ltnled 
 |-  ( ph -> ( ( V + 1 ) < ( ( V + 1 ) + 1 ) <-> -. ( ( V + 1 ) + 1 ) <_ ( V + 1 ) ) )
46 42 45 mpbid 
 |-  ( ph -> -. ( ( V + 1 ) + 1 ) <_ ( V + 1 ) )
47 elfzle1 
 |-  ( ( V + 1 ) e. ( ( ( V + 1 ) + 1 ) ... N ) -> ( ( V + 1 ) + 1 ) <_ ( V + 1 ) )
48 46 47 nsyl 
 |-  ( ph -> -. ( V + 1 ) e. ( ( ( V + 1 ) + 1 ) ... N ) )
49 difsn 
 |-  ( -. ( V + 1 ) e. ( ( ( V + 1 ) + 1 ) ... N ) -> ( ( ( ( V + 1 ) + 1 ) ... N ) \ { ( V + 1 ) } ) = ( ( ( V + 1 ) + 1 ) ... N ) )
50 48 49 syl 
 |-  ( ph -> ( ( ( ( V + 1 ) + 1 ) ... N ) \ { ( V + 1 ) } ) = ( ( ( V + 1 ) + 1 ) ... N ) )
51 41 50 uneq12d 
 |-  ( ph -> ( ( ( 1 ... ( V + 1 ) ) \ { ( V + 1 ) } ) u. ( ( ( ( V + 1 ) + 1 ) ... N ) \ { ( V + 1 ) } ) ) = ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) )
52 22 51 eqtrid 
 |-  ( ph -> ( ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) \ { ( V + 1 ) } ) = ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) )
53 21 52 eqtrd 
 |-  ( ph -> ( ( 1 ... N ) \ { ( V + 1 ) } ) = ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) )
54 53 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { ( V + 1 ) } ) ) = ( U " ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
55 11 54 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) = ( U " ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
56 imaundi 
 |-  ( U " ( ( 1 ... V ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... V ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) )
57 55 56 eqtrdi 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) = ( ( U " ( 1 ... V ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
58 57 eleq2d 
 |-  ( ph -> ( n e. ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) <-> n e. ( ( U " ( 1 ... V ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) )
59 eldif 
 |-  ( n e. ( ( U " ( 1 ... N ) ) \ ( U " { ( V + 1 ) } ) ) <-> ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { ( V + 1 ) } ) ) )
60 elun 
 |-  ( n e. ( ( U " ( 1 ... V ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) <-> ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
61 58 59 60 3bitr3g 
 |-  ( ph -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { ( V + 1 ) } ) ) <-> ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) )
62 61 adantr 
 |-  ( ( ph /\ M < V ) -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { ( V + 1 ) } ) ) <-> ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) )
63 imassrn 
 |-  ( U " ( 1 ... V ) ) C_ ran U
64 f1of 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) --> ( 1 ... N ) )
65 4 64 syl 
 |-  ( ph -> U : ( 1 ... N ) --> ( 1 ... N ) )
66 65 frnd 
 |-  ( ph -> ran U C_ ( 1 ... N ) )
67 63 66 sstrid 
 |-  ( ph -> ( U " ( 1 ... V ) ) C_ ( 1 ... N ) )
68 67 sselda 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> n e. ( 1 ... N ) )
69 3 ffnd 
 |-  ( ph -> T Fn ( 1 ... N ) )
70 69 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> T Fn ( 1 ... N ) )
71 1ex 
 |-  1 e. _V
72 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) ) )
73 71 72 ax-mp 
 |-  ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) )
74 c0ex 
 |-  0 e. _V
75 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) ) )
76 74 75 ax-mp 
 |-  ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) )
77 73 76 pm3.2i 
 |-  ( ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) ) /\ ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) ) )
78 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) ) = ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) )
79 9 78 syl 
 |-  ( ph -> ( U " ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) ) = ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) )
80 fzdisj 
 |-  ( V < ( V + 1 ) -> ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) = (/) )
81 31 80 syl 
 |-  ( ph -> ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) = (/) )
82 81 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) ) = ( U " (/) ) )
83 ima0 
 |-  ( U " (/) ) = (/)
84 82 83 eqtrdi 
 |-  ( ph -> ( U " ( ( 1 ... V ) i^i ( ( V + 1 ) ... N ) ) ) = (/) )
85 79 84 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) )
86 fnun 
 |-  ( ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) ) /\ ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) ) ) /\ ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... V ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) )
87 77 85 86 sylancr 
 |-  ( ph -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... V ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) )
88 imaundi 
 |-  ( U " ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) ) = ( ( U " ( 1 ... V ) ) u. ( U " ( ( V + 1 ) ... N ) ) )
89 1 nnzd 
 |-  ( ph -> N e. ZZ )
90 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
91 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
92 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
93 89 90 91 92 4syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
94 16 93 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
95 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
96 94 95 syl 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
97 96 5 sseldd 
 |-  ( ph -> V e. ( 1 ... N ) )
98 fzsplit 
 |-  ( V e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) )
99 97 98 syl 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) )
100 99 imaeq2d 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) ) )
101 f1ofo 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
102 4 101 syl 
 |-  ( ph -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
103 foima 
 |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
104 102 103 syl 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
105 100 104 eqtr3d 
 |-  ( ph -> ( U " ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) ) = ( 1 ... N ) )
106 88 105 eqtr3id 
 |-  ( ph -> ( ( U " ( 1 ... V ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) = ( 1 ... N ) )
107 106 fneq2d 
 |-  ( ph -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... V ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) <-> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
108 87 107 mpbid 
 |-  ( ph -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
109 108 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
110 fzfid 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( 1 ... N ) e. Fin )
111 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
112 eqidd 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( T ` n ) = ( T ` n ) )
113 fvun1 
 |-  ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) ) /\ ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... V ) ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... V ) ) X. { 1 } ) ` n ) )
114 73 76 113 mp3an12 
 |-  ( ( ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... V ) ) X. { 1 } ) ` n ) )
115 85 114 sylan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... V ) ) X. { 1 } ) ` n ) )
116 71 fvconst2 
 |-  ( n e. ( U " ( 1 ... V ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) ` n ) = 1 )
117 116 adantl 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) ` n ) = 1 )
118 115 117 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
119 118 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
120 70 109 110 110 111 112 119 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
121 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) ) )
122 71 121 ax-mp 
 |-  ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) )
123 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) )
124 74 123 ax-mp 
 |-  ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) )
125 122 124 pm3.2i 
 |-  ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) ) /\ ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) )
126 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
127 9 126 syl 
 |-  ( ph -> ( U " ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
128 fzdisj 
 |-  ( ( V + 1 ) < ( ( V + 1 ) + 1 ) -> ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) = (/) )
129 42 128 syl 
 |-  ( ph -> ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) = (/) )
130 129 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( U " (/) ) )
131 130 83 eqtrdi 
 |-  ( ph -> ( U " ( ( 1 ... ( V + 1 ) ) i^i ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) )
132 127 131 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) )
133 fnun 
 |-  ( ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) ) /\ ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V + 1 ) ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
134 125 132 133 sylancr 
 |-  ( ph -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V + 1 ) ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
135 imaundi 
 |-  ( U " ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( V + 1 ) ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) )
136 20 imaeq2d 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) )
137 136 104 eqtr3d 
 |-  ( ph -> ( U " ( ( 1 ... ( V + 1 ) ) u. ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
138 135 137 eqtr3id 
 |-  ( ph -> ( ( U " ( 1 ... ( V + 1 ) ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
139 138 fneq2d 
 |-  ( ph -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V + 1 ) ) ) u. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) <-> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
140 134 139 mpbid 
 |-  ( ph -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
141 140 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
142 uzid 
 |-  ( V e. ZZ -> V e. ( ZZ>= ` V ) )
143 29 142 syl 
 |-  ( ph -> V e. ( ZZ>= ` V ) )
144 peano2uz 
 |-  ( V e. ( ZZ>= ` V ) -> ( V + 1 ) e. ( ZZ>= ` V ) )
145 fzss2 
 |-  ( ( V + 1 ) e. ( ZZ>= ` V ) -> ( 1 ... V ) C_ ( 1 ... ( V + 1 ) ) )
146 imass2 
 |-  ( ( 1 ... V ) C_ ( 1 ... ( V + 1 ) ) -> ( U " ( 1 ... V ) ) C_ ( U " ( 1 ... ( V + 1 ) ) ) )
147 143 144 145 146 4syl 
 |-  ( ph -> ( U " ( 1 ... V ) ) C_ ( U " ( 1 ... ( V + 1 ) ) ) )
148 147 sselda 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> n e. ( U " ( 1 ... ( V + 1 ) ) ) )
149 fvun1 
 |-  ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) ) /\ ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( V + 1 ) ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) ` n ) )
150 122 124 149 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( V + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) ` n ) )
151 132 150 sylan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) ` n ) )
152 71 fvconst2 
 |-  ( n e. ( U " ( 1 ... ( V + 1 ) ) ) -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) ` n ) = 1 )
153 152 adantl 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V + 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) ` n ) = 1 )
154 151 153 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
155 148 154 syldan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
156 155 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
157 70 141 110 110 111 112 156 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
158 120 157 eqtr4d 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
159 68 158 mpdan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... V ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
160 imassrn 
 |-  ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) C_ ran U
161 160 66 sstrid 
 |-  ( ph -> ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) C_ ( 1 ... N ) )
162 161 sselda 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> n e. ( 1 ... N ) )
163 69 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> T Fn ( 1 ... N ) )
164 108 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
165 fzfid 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( 1 ... N ) e. Fin )
166 eqidd 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( T ` n ) = ( T ` n ) )
167 uzid 
 |-  ( ( V + 1 ) e. ZZ -> ( V + 1 ) e. ( ZZ>= ` ( V + 1 ) ) )
168 32 167 syl 
 |-  ( ph -> ( V + 1 ) e. ( ZZ>= ` ( V + 1 ) ) )
169 peano2uz 
 |-  ( ( V + 1 ) e. ( ZZ>= ` ( V + 1 ) ) -> ( ( V + 1 ) + 1 ) e. ( ZZ>= ` ( V + 1 ) ) )
170 fzss1 
 |-  ( ( ( V + 1 ) + 1 ) e. ( ZZ>= ` ( V + 1 ) ) -> ( ( ( V + 1 ) + 1 ) ... N ) C_ ( ( V + 1 ) ... N ) )
171 imass2 
 |-  ( ( ( ( V + 1 ) + 1 ) ... N ) C_ ( ( V + 1 ) ... N ) -> ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) C_ ( U " ( ( V + 1 ) ... N ) ) )
172 168 169 170 171 4syl 
 |-  ( ph -> ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) C_ ( U " ( ( V + 1 ) ... N ) ) )
173 172 sselda 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> n e. ( U " ( ( V + 1 ) ... N ) ) )
174 fvun2 
 |-  ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) Fn ( U " ( 1 ... V ) ) /\ ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( V + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ` n ) )
175 73 76 174 mp3an12 
 |-  ( ( ( ( U " ( 1 ... V ) ) i^i ( U " ( ( V + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ` n ) )
176 85 175 sylan 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ` n ) )
177 74 fvconst2 
 |-  ( n e. ( U " ( ( V + 1 ) ... N ) ) -> ( ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ` n ) = 0 )
178 177 adantl 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ` n ) = 0 )
179 176 178 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
180 173 179 syldan 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
181 180 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
182 163 164 165 165 111 166 181 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
183 140 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
184 fvun2 
 |-  ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V + 1 ) ) ) /\ ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ` n ) )
185 122 124 184 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) i^i ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ` n ) )
186 132 185 sylan 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ` n ) )
187 74 fvconst2 
 |-  ( n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) -> ( ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ` n ) = 0 )
188 187 adantl 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ` n ) = 0 )
189 186 188 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
190 189 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
191 163 183 165 165 111 166 190 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
192 182 191 eqtr4d 
 |-  ( ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
193 162 192 mpdan 
 |-  ( ( ph /\ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
194 159 193 jaodan 
 |-  ( ( ph /\ ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
195 194 adantlr 
 |-  ( ( ( ph /\ M < V ) /\ ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
196 2 adantr 
 |-  ( ( ph /\ M < V ) -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
197 vex 
 |-  y e. _V
198 ovex 
 |-  ( y + 1 ) e. _V
199 197 198 ifex 
 |-  if ( y < M , y , ( y + 1 ) ) e. _V
200 199 a1i 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) e. _V )
201 breq1 
 |-  ( y = ( V - 1 ) -> ( y < M <-> ( V - 1 ) < M ) )
202 201 adantl 
 |-  ( ( ph /\ y = ( V - 1 ) ) -> ( y < M <-> ( V - 1 ) < M ) )
203 simpr 
 |-  ( ( ph /\ y = ( V - 1 ) ) -> y = ( V - 1 ) )
204 oveq1 
 |-  ( y = ( V - 1 ) -> ( y + 1 ) = ( ( V - 1 ) + 1 ) )
205 29 zcnd 
 |-  ( ph -> V e. CC )
206 npcan1 
 |-  ( V e. CC -> ( ( V - 1 ) + 1 ) = V )
207 205 206 syl 
 |-  ( ph -> ( ( V - 1 ) + 1 ) = V )
208 204 207 sylan9eqr 
 |-  ( ( ph /\ y = ( V - 1 ) ) -> ( y + 1 ) = V )
209 202 203 208 ifbieq12d 
 |-  ( ( ph /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = if ( ( V - 1 ) < M , ( V - 1 ) , V ) )
210 209 adantlr 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = if ( ( V - 1 ) < M , ( V - 1 ) , V ) )
211 6 eldifad 
 |-  ( ph -> M e. ( 0 ... N ) )
212 211 elfzelzd 
 |-  ( ph -> M e. ZZ )
213 zltlem1 
 |-  ( ( M e. ZZ /\ V e. ZZ ) -> ( M < V <-> M <_ ( V - 1 ) ) )
214 212 29 213 syl2anc 
 |-  ( ph -> ( M < V <-> M <_ ( V - 1 ) ) )
215 212 zred 
 |-  ( ph -> M e. RR )
216 peano2zm 
 |-  ( V e. ZZ -> ( V - 1 ) e. ZZ )
217 29 216 syl 
 |-  ( ph -> ( V - 1 ) e. ZZ )
218 217 zred 
 |-  ( ph -> ( V - 1 ) e. RR )
219 215 218 lenltd 
 |-  ( ph -> ( M <_ ( V - 1 ) <-> -. ( V - 1 ) < M ) )
220 214 219 bitrd 
 |-  ( ph -> ( M < V <-> -. ( V - 1 ) < M ) )
221 220 biimpa 
 |-  ( ( ph /\ M < V ) -> -. ( V - 1 ) < M )
222 221 iffalsed 
 |-  ( ( ph /\ M < V ) -> if ( ( V - 1 ) < M , ( V - 1 ) , V ) = V )
223 222 adantr 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> if ( ( V - 1 ) < M , ( V - 1 ) , V ) = V )
224 210 223 eqtrd 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = V )
225 224 eqeq2d 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> ( j = if ( y < M , y , ( y + 1 ) ) <-> j = V ) )
226 225 biimpa 
 |-  ( ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> j = V )
227 oveq2 
 |-  ( j = V -> ( 1 ... j ) = ( 1 ... V ) )
228 227 imaeq2d 
 |-  ( j = V -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... V ) ) )
229 228 xpeq1d 
 |-  ( j = V -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... V ) ) X. { 1 } ) )
230 oveq1 
 |-  ( j = V -> ( j + 1 ) = ( V + 1 ) )
231 230 oveq1d 
 |-  ( j = V -> ( ( j + 1 ) ... N ) = ( ( V + 1 ) ... N ) )
232 231 imaeq2d 
 |-  ( j = V -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( ( V + 1 ) ... N ) ) )
233 232 xpeq1d 
 |-  ( j = V -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) )
234 229 233 uneq12d 
 |-  ( j = V -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) )
235 234 oveq2d 
 |-  ( j = V -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
236 226 235 syl 
 |-  ( ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
237 200 236 csbied 
 |-  ( ( ( ph /\ M < V ) /\ y = ( V - 1 ) ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
238 elfzm1b 
 |-  ( ( V e. ZZ /\ N e. ZZ ) -> ( V e. ( 1 ... N ) <-> ( V - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
239 29 89 238 syl2anc 
 |-  ( ph -> ( V e. ( 1 ... N ) <-> ( V - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
240 97 239 mpbid 
 |-  ( ph -> ( V - 1 ) e. ( 0 ... ( N - 1 ) ) )
241 240 adantr 
 |-  ( ( ph /\ M < V ) -> ( V - 1 ) e. ( 0 ... ( N - 1 ) ) )
242 ovexd 
 |-  ( ( ph /\ M < V ) -> ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
243 196 237 241 242 fvmptd 
 |-  ( ( ph /\ M < V ) -> ( F ` ( V - 1 ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
244 243 fveq1d 
 |-  ( ( ph /\ M < V ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
245 244 adantr 
 |-  ( ( ( ph /\ M < V ) /\ ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
246 199 a1i 
 |-  ( ( ( ph /\ M < V ) /\ y = V ) -> if ( y < M , y , ( y + 1 ) ) e. _V )
247 breq1 
 |-  ( y = V -> ( y < M <-> V < M ) )
248 id 
 |-  ( y = V -> y = V )
249 oveq1 
 |-  ( y = V -> ( y + 1 ) = ( V + 1 ) )
250 247 248 249 ifbieq12d 
 |-  ( y = V -> if ( y < M , y , ( y + 1 ) ) = if ( V < M , V , ( V + 1 ) ) )
251 ltnsym 
 |-  ( ( M e. RR /\ V e. RR ) -> ( M < V -> -. V < M ) )
252 215 30 251 syl2anc 
 |-  ( ph -> ( M < V -> -. V < M ) )
253 252 imp 
 |-  ( ( ph /\ M < V ) -> -. V < M )
254 253 iffalsed 
 |-  ( ( ph /\ M < V ) -> if ( V < M , V , ( V + 1 ) ) = ( V + 1 ) )
255 250 254 sylan9eqr 
 |-  ( ( ( ph /\ M < V ) /\ y = V ) -> if ( y < M , y , ( y + 1 ) ) = ( V + 1 ) )
256 255 eqeq2d 
 |-  ( ( ( ph /\ M < V ) /\ y = V ) -> ( j = if ( y < M , y , ( y + 1 ) ) <-> j = ( V + 1 ) ) )
257 256 biimpa 
 |-  ( ( ( ( ph /\ M < V ) /\ y = V ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> j = ( V + 1 ) )
258 oveq2 
 |-  ( j = ( V + 1 ) -> ( 1 ... j ) = ( 1 ... ( V + 1 ) ) )
259 258 imaeq2d 
 |-  ( j = ( V + 1 ) -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... ( V + 1 ) ) ) )
260 259 xpeq1d 
 |-  ( j = ( V + 1 ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) )
261 oveq1 
 |-  ( j = ( V + 1 ) -> ( j + 1 ) = ( ( V + 1 ) + 1 ) )
262 261 oveq1d 
 |-  ( j = ( V + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( V + 1 ) + 1 ) ... N ) )
263 262 imaeq2d 
 |-  ( j = ( V + 1 ) -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) )
264 263 xpeq1d 
 |-  ( j = ( V + 1 ) -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
265 260 264 uneq12d 
 |-  ( j = ( V + 1 ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
266 265 oveq2d 
 |-  ( j = ( V + 1 ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
267 257 266 syl 
 |-  ( ( ( ( ph /\ M < V ) /\ y = V ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
268 246 267 csbied 
 |-  ( ( ( ph /\ M < V ) /\ y = V ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
269 fz1ssfz0 
 |-  ( 1 ... ( N - 1 ) ) C_ ( 0 ... ( N - 1 ) )
270 269 5 sselid 
 |-  ( ph -> V e. ( 0 ... ( N - 1 ) ) )
271 270 adantr 
 |-  ( ( ph /\ M < V ) -> V e. ( 0 ... ( N - 1 ) ) )
272 ovexd 
 |-  ( ( ph /\ M < V ) -> ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
273 196 268 271 272 fvmptd 
 |-  ( ( ph /\ M < V ) -> ( F ` V ) = ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
274 273 fveq1d 
 |-  ( ( ph /\ M < V ) -> ( ( F ` V ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
275 274 adantr 
 |-  ( ( ( ph /\ M < V ) /\ ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( F ` V ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
276 195 245 275 3eqtr4d 
 |-  ( ( ( ph /\ M < V ) /\ ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) )
277 276 ex 
 |-  ( ( ph /\ M < V ) -> ( ( n e. ( U " ( 1 ... V ) ) \/ n e. ( U " ( ( ( V + 1 ) + 1 ) ... N ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
278 62 277 sylbid 
 |-  ( ( ph /\ M < V ) -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { ( V + 1 ) } ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
279 278 expdimp 
 |-  ( ( ( ph /\ M < V ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( -. n e. ( U " { ( V + 1 ) } ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
280 279 necon1ad 
 |-  ( ( ( ph /\ M < V ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n e. ( U " { ( V + 1 ) } ) ) )
281 elimasni 
 |-  ( n e. ( U " { ( V + 1 ) } ) -> ( V + 1 ) U n )
282 eqcom 
 |-  ( n = ( U ` ( V + 1 ) ) <-> ( U ` ( V + 1 ) ) = n )
283 f1ofn 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U Fn ( 1 ... N ) )
284 4 283 syl 
 |-  ( ph -> U Fn ( 1 ... N ) )
285 fnbrfvb 
 |-  ( ( U Fn ( 1 ... N ) /\ ( V + 1 ) e. ( 1 ... N ) ) -> ( ( U ` ( V + 1 ) ) = n <-> ( V + 1 ) U n ) )
286 284 18 285 syl2anc 
 |-  ( ph -> ( ( U ` ( V + 1 ) ) = n <-> ( V + 1 ) U n ) )
287 282 286 bitrid 
 |-  ( ph -> ( n = ( U ` ( V + 1 ) ) <-> ( V + 1 ) U n ) )
288 281 287 imbitrrid 
 |-  ( ph -> ( n e. ( U " { ( V + 1 ) } ) -> n = ( U ` ( V + 1 ) ) ) )
289 288 ad2antrr 
 |-  ( ( ( ph /\ M < V ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( n e. ( U " { ( V + 1 ) } ) -> n = ( U ` ( V + 1 ) ) ) )
290 280 289 syld 
 |-  ( ( ( ph /\ M < V ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` ( V + 1 ) ) ) )
291 290 ralrimiva 
 |-  ( ( ph /\ M < V ) -> A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` ( V + 1 ) ) ) )
292 fvex 
 |-  ( U ` ( V + 1 ) ) e. _V
293 eqeq2 
 |-  ( m = ( U ` ( V + 1 ) ) -> ( n = m <-> n = ( U ` ( V + 1 ) ) ) )
294 293 imbi2d 
 |-  ( m = ( U ` ( V + 1 ) ) -> ( ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) <-> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` ( V + 1 ) ) ) ) )
295 294 ralbidv 
 |-  ( m = ( U ` ( V + 1 ) ) -> ( A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) <-> A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` ( V + 1 ) ) ) ) )
296 292 295 spcev 
 |-  ( A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` ( V + 1 ) ) ) -> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
297 291 296 syl 
 |-  ( ( ph /\ M < V ) -> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
298 imadif 
 |-  ( Fun `' U -> ( U " ( ( 1 ... N ) \ { V } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) )
299 9 298 syl 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { V } ) ) = ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) )
300 99 difeq1d 
 |-  ( ph -> ( ( 1 ... N ) \ { V } ) = ( ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) \ { V } ) )
301 difundir 
 |-  ( ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) \ { V } ) = ( ( ( 1 ... V ) \ { V } ) u. ( ( ( V + 1 ) ... N ) \ { V } ) )
302 207 24 eqeltrd 
 |-  ( ph -> ( ( V - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
303 uzid 
 |-  ( ( V - 1 ) e. ZZ -> ( V - 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
304 peano2uz 
 |-  ( ( V - 1 ) e. ( ZZ>= ` ( V - 1 ) ) -> ( ( V - 1 ) + 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
305 29 216 303 304 4syl 
 |-  ( ph -> ( ( V - 1 ) + 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
306 207 305 eqeltrrd 
 |-  ( ph -> V e. ( ZZ>= ` ( V - 1 ) ) )
307 fzsplit2 
 |-  ( ( ( ( V - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ V e. ( ZZ>= ` ( V - 1 ) ) ) -> ( 1 ... V ) = ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... V ) ) )
308 302 306 307 syl2anc 
 |-  ( ph -> ( 1 ... V ) = ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... V ) ) )
309 207 oveq1d 
 |-  ( ph -> ( ( ( V - 1 ) + 1 ) ... V ) = ( V ... V ) )
310 fzsn 
 |-  ( V e. ZZ -> ( V ... V ) = { V } )
311 29 310 syl 
 |-  ( ph -> ( V ... V ) = { V } )
312 309 311 eqtrd 
 |-  ( ph -> ( ( ( V - 1 ) + 1 ) ... V ) = { V } )
313 312 uneq2d 
 |-  ( ph -> ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... V ) ) = ( ( 1 ... ( V - 1 ) ) u. { V } ) )
314 308 313 eqtrd 
 |-  ( ph -> ( 1 ... V ) = ( ( 1 ... ( V - 1 ) ) u. { V } ) )
315 314 difeq1d 
 |-  ( ph -> ( ( 1 ... V ) \ { V } ) = ( ( ( 1 ... ( V - 1 ) ) u. { V } ) \ { V } ) )
316 difun2 
 |-  ( ( ( 1 ... ( V - 1 ) ) u. { V } ) \ { V } ) = ( ( 1 ... ( V - 1 ) ) \ { V } )
317 30 ltm1d 
 |-  ( ph -> ( V - 1 ) < V )
318 218 30 ltnled 
 |-  ( ph -> ( ( V - 1 ) < V <-> -. V <_ ( V - 1 ) ) )
319 317 318 mpbid 
 |-  ( ph -> -. V <_ ( V - 1 ) )
320 elfzle2 
 |-  ( V e. ( 1 ... ( V - 1 ) ) -> V <_ ( V - 1 ) )
321 319 320 nsyl 
 |-  ( ph -> -. V e. ( 1 ... ( V - 1 ) ) )
322 difsn 
 |-  ( -. V e. ( 1 ... ( V - 1 ) ) -> ( ( 1 ... ( V - 1 ) ) \ { V } ) = ( 1 ... ( V - 1 ) ) )
323 321 322 syl 
 |-  ( ph -> ( ( 1 ... ( V - 1 ) ) \ { V } ) = ( 1 ... ( V - 1 ) ) )
324 316 323 eqtrid 
 |-  ( ph -> ( ( ( 1 ... ( V - 1 ) ) u. { V } ) \ { V } ) = ( 1 ... ( V - 1 ) ) )
325 315 324 eqtrd 
 |-  ( ph -> ( ( 1 ... V ) \ { V } ) = ( 1 ... ( V - 1 ) ) )
326 elfzle1 
 |-  ( V e. ( ( V + 1 ) ... N ) -> ( V + 1 ) <_ V )
327 35 326 nsyl 
 |-  ( ph -> -. V e. ( ( V + 1 ) ... N ) )
328 difsn 
 |-  ( -. V e. ( ( V + 1 ) ... N ) -> ( ( ( V + 1 ) ... N ) \ { V } ) = ( ( V + 1 ) ... N ) )
329 327 328 syl 
 |-  ( ph -> ( ( ( V + 1 ) ... N ) \ { V } ) = ( ( V + 1 ) ... N ) )
330 325 329 uneq12d 
 |-  ( ph -> ( ( ( 1 ... V ) \ { V } ) u. ( ( ( V + 1 ) ... N ) \ { V } ) ) = ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) )
331 301 330 eqtrid 
 |-  ( ph -> ( ( ( 1 ... V ) u. ( ( V + 1 ) ... N ) ) \ { V } ) = ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) )
332 300 331 eqtrd 
 |-  ( ph -> ( ( 1 ... N ) \ { V } ) = ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) )
333 332 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... N ) \ { V } ) ) = ( U " ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) ) )
334 299 333 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) = ( U " ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) ) )
335 imaundi 
 |-  ( U " ( ( 1 ... ( V - 1 ) ) u. ( ( V + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( ( V + 1 ) ... N ) ) )
336 334 335 eqtrdi 
 |-  ( ph -> ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) = ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) )
337 336 eleq2d 
 |-  ( ph -> ( n e. ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) <-> n e. ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) ) )
338 eldif 
 |-  ( n e. ( ( U " ( 1 ... N ) ) \ ( U " { V } ) ) <-> ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { V } ) ) )
339 elun 
 |-  ( n e. ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( ( V + 1 ) ... N ) ) ) <-> ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) )
340 337 338 339 3bitr3g 
 |-  ( ph -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { V } ) ) <-> ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) )
341 340 adantr 
 |-  ( ( ph /\ V < M ) -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { V } ) ) <-> ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) )
342 imassrn 
 |-  ( U " ( 1 ... ( V - 1 ) ) ) C_ ran U
343 342 66 sstrid 
 |-  ( ph -> ( U " ( 1 ... ( V - 1 ) ) ) C_ ( 1 ... N ) )
344 343 sselda 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> n e. ( 1 ... N ) )
345 69 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> T Fn ( 1 ... N ) )
346 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) ) )
347 71 346 ax-mp 
 |-  ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) )
348 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) ) )
349 74 348 ax-mp 
 |-  ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) )
350 347 349 pm3.2i 
 |-  ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) ) /\ ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) ) )
351 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) ) = ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) )
352 9 351 syl 
 |-  ( ph -> ( U " ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) ) = ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) )
353 fzdisj 
 |-  ( ( V - 1 ) < V -> ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) = (/) )
354 317 353 syl 
 |-  ( ph -> ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) = (/) )
355 354 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) ) = ( U " (/) ) )
356 355 83 eqtrdi 
 |-  ( ph -> ( U " ( ( 1 ... ( V - 1 ) ) i^i ( V ... N ) ) ) = (/) )
357 352 356 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) )
358 fnun 
 |-  ( ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) ) /\ ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) ) ) /\ ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( V ... N ) ) ) )
359 350 357 358 sylancr 
 |-  ( ph -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( V ... N ) ) ) )
360 imaundi 
 |-  ( U " ( ( 1 ... ( V - 1 ) ) u. ( V ... N ) ) ) = ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( V ... N ) ) )
361 uzss 
 |-  ( V e. ( ZZ>= ` ( V - 1 ) ) -> ( ZZ>= ` V ) C_ ( ZZ>= ` ( V - 1 ) ) )
362 306 361 syl 
 |-  ( ph -> ( ZZ>= ` V ) C_ ( ZZ>= ` ( V - 1 ) ) )
363 elfzuz3 
 |-  ( V e. ( 1 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` V ) )
364 5 363 syl 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` V ) )
365 362 364 sseldd 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
366 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( V - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
367 365 366 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( V - 1 ) ) )
368 16 367 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( V - 1 ) ) )
369 fzsplit2 
 |-  ( ( ( ( V - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( V - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... N ) ) )
370 302 368 369 syl2anc 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... N ) ) )
371 207 oveq1d 
 |-  ( ph -> ( ( ( V - 1 ) + 1 ) ... N ) = ( V ... N ) )
372 371 uneq2d 
 |-  ( ph -> ( ( 1 ... ( V - 1 ) ) u. ( ( ( V - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( V - 1 ) ) u. ( V ... N ) ) )
373 370 372 eqtrd 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( V - 1 ) ) u. ( V ... N ) ) )
374 373 imaeq2d 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... ( V - 1 ) ) u. ( V ... N ) ) ) )
375 374 104 eqtr3d 
 |-  ( ph -> ( U " ( ( 1 ... ( V - 1 ) ) u. ( V ... N ) ) ) = ( 1 ... N ) )
376 360 375 eqtr3id 
 |-  ( ph -> ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( V ... N ) ) ) = ( 1 ... N ) )
377 376 fneq2d 
 |-  ( ph -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( V - 1 ) ) ) u. ( U " ( V ... N ) ) ) <-> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
378 359 377 mpbid 
 |-  ( ph -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
379 378 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
380 fzfid 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( 1 ... N ) e. Fin )
381 eqidd 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( T ` n ) = ( T ` n ) )
382 fvun1 
 |-  ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) ) /\ ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) ) /\ ( ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) ` n ) )
383 347 349 382 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) ` n ) )
384 357 383 sylan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) ` n ) )
385 71 fvconst2 
 |-  ( n e. ( U " ( 1 ... ( V - 1 ) ) ) -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) ` n ) = 1 )
386 385 adantl 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) ` n ) = 1 )
387 384 386 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = 1 )
388 387 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = 1 )
389 345 379 380 380 111 381 388 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
390 108 adantr 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
391 fzss2 
 |-  ( V e. ( ZZ>= ` ( V - 1 ) ) -> ( 1 ... ( V - 1 ) ) C_ ( 1 ... V ) )
392 306 391 syl 
 |-  ( ph -> ( 1 ... ( V - 1 ) ) C_ ( 1 ... V ) )
393 imass2 
 |-  ( ( 1 ... ( V - 1 ) ) C_ ( 1 ... V ) -> ( U " ( 1 ... ( V - 1 ) ) ) C_ ( U " ( 1 ... V ) ) )
394 392 393 syl 
 |-  ( ph -> ( U " ( 1 ... ( V - 1 ) ) ) C_ ( U " ( 1 ... V ) ) )
395 394 sselda 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> n e. ( U " ( 1 ... V ) ) )
396 395 118 syldan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
397 396 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
398 345 390 380 380 111 381 397 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
399 389 398 eqtr4d 
 |-  ( ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
400 344 399 mpdan 
 |-  ( ( ph /\ n e. ( U " ( 1 ... ( V - 1 ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
401 imassrn 
 |-  ( U " ( ( V + 1 ) ... N ) ) C_ ran U
402 401 66 sstrid 
 |-  ( ph -> ( U " ( ( V + 1 ) ... N ) ) C_ ( 1 ... N ) )
403 402 sselda 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> n e. ( 1 ... N ) )
404 69 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> T Fn ( 1 ... N ) )
405 378 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
406 fzfid 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( 1 ... N ) e. Fin )
407 eqidd 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( T ` n ) = ( T ` n ) )
408 fzss1 
 |-  ( ( V + 1 ) e. ( ZZ>= ` V ) -> ( ( V + 1 ) ... N ) C_ ( V ... N ) )
409 imass2 
 |-  ( ( ( V + 1 ) ... N ) C_ ( V ... N ) -> ( U " ( ( V + 1 ) ... N ) ) C_ ( U " ( V ... N ) ) )
410 143 144 408 409 4syl 
 |-  ( ph -> ( U " ( ( V + 1 ) ... N ) ) C_ ( U " ( V ... N ) ) )
411 410 sselda 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> n e. ( U " ( V ... N ) ) )
412 fvun2 
 |-  ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( V - 1 ) ) ) /\ ( ( U " ( V ... N ) ) X. { 0 } ) Fn ( U " ( V ... N ) ) /\ ( ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) /\ n e. ( U " ( V ... N ) ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( V ... N ) ) X. { 0 } ) ` n ) )
413 347 349 412 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) i^i ( U " ( V ... N ) ) ) = (/) /\ n e. ( U " ( V ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( V ... N ) ) X. { 0 } ) ` n ) )
414 357 413 sylan 
 |-  ( ( ph /\ n e. ( U " ( V ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( V ... N ) ) X. { 0 } ) ` n ) )
415 74 fvconst2 
 |-  ( n e. ( U " ( V ... N ) ) -> ( ( ( U " ( V ... N ) ) X. { 0 } ) ` n ) = 0 )
416 415 adantl 
 |-  ( ( ph /\ n e. ( U " ( V ... N ) ) ) -> ( ( ( U " ( V ... N ) ) X. { 0 } ) ` n ) = 0 )
417 414 416 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( V ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = 0 )
418 411 417 syldan 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = 0 )
419 418 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ` n ) = 0 )
420 404 405 406 406 111 407 419 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
421 108 adantr 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
422 179 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 0 )
423 404 421 406 406 111 407 422 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
424 420 423 eqtr4d 
 |-  ( ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
425 403 424 mpdan 
 |-  ( ( ph /\ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
426 400 425 jaodan 
 |-  ( ( ph /\ ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
427 426 adantlr 
 |-  ( ( ( ph /\ V < M ) /\ ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
428 2 adantr 
 |-  ( ( ph /\ V < M ) -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
429 199 a1i 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) e. _V )
430 209 adantlr 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = if ( ( V - 1 ) < M , ( V - 1 ) , V ) )
431 lttr 
 |-  ( ( ( V - 1 ) e. RR /\ V e. RR /\ M e. RR ) -> ( ( ( V - 1 ) < V /\ V < M ) -> ( V - 1 ) < M ) )
432 218 30 215 431 syl3anc 
 |-  ( ph -> ( ( ( V - 1 ) < V /\ V < M ) -> ( V - 1 ) < M ) )
433 317 432 mpand 
 |-  ( ph -> ( V < M -> ( V - 1 ) < M ) )
434 433 imp 
 |-  ( ( ph /\ V < M ) -> ( V - 1 ) < M )
435 434 iftrued 
 |-  ( ( ph /\ V < M ) -> if ( ( V - 1 ) < M , ( V - 1 ) , V ) = ( V - 1 ) )
436 435 adantr 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> if ( ( V - 1 ) < M , ( V - 1 ) , V ) = ( V - 1 ) )
437 430 436 eqtrd 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = ( V - 1 ) )
438 simpll 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> ph )
439 oveq2 
 |-  ( j = ( V - 1 ) -> ( 1 ... j ) = ( 1 ... ( V - 1 ) ) )
440 439 imaeq2d 
 |-  ( j = ( V - 1 ) -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... ( V - 1 ) ) ) )
441 440 xpeq1d 
 |-  ( j = ( V - 1 ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) )
442 441 adantl 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) )
443 oveq1 
 |-  ( j = ( V - 1 ) -> ( j + 1 ) = ( ( V - 1 ) + 1 ) )
444 443 207 sylan9eqr 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( j + 1 ) = V )
445 444 oveq1d 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( ( j + 1 ) ... N ) = ( V ... N ) )
446 445 imaeq2d 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( V ... N ) ) )
447 446 xpeq1d 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( V ... N ) ) X. { 0 } ) )
448 442 447 uneq12d 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) )
449 448 oveq2d 
 |-  ( ( ph /\ j = ( V - 1 ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) )
450 438 449 sylan 
 |-  ( ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) /\ j = ( V - 1 ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) )
451 429 437 450 csbied2 
 |-  ( ( ( ph /\ V < M ) /\ y = ( V - 1 ) ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) )
452 240 adantr 
 |-  ( ( ph /\ V < M ) -> ( V - 1 ) e. ( 0 ... ( N - 1 ) ) )
453 ovexd 
 |-  ( ( ph /\ V < M ) -> ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) e. _V )
454 428 451 452 453 fvmptd 
 |-  ( ( ph /\ V < M ) -> ( F ` ( V - 1 ) ) = ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) )
455 454 fveq1d 
 |-  ( ( ph /\ V < M ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) )
456 455 adantr 
 |-  ( ( ( ph /\ V < M ) /\ ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( V - 1 ) ) ) X. { 1 } ) u. ( ( U " ( V ... N ) ) X. { 0 } ) ) ) ` n ) )
457 199 a1i 
 |-  ( ( V < M /\ y = V ) -> if ( y < M , y , ( y + 1 ) ) e. _V )
458 iftrue 
 |-  ( V < M -> if ( V < M , V , ( V + 1 ) ) = V )
459 250 458 sylan9eqr 
 |-  ( ( V < M /\ y = V ) -> if ( y < M , y , ( y + 1 ) ) = V )
460 459 eqeq2d 
 |-  ( ( V < M /\ y = V ) -> ( j = if ( y < M , y , ( y + 1 ) ) <-> j = V ) )
461 460 biimpa 
 |-  ( ( ( V < M /\ y = V ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> j = V )
462 461 235 syl 
 |-  ( ( ( V < M /\ y = V ) /\ j = if ( y < M , y , ( y + 1 ) ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
463 457 462 csbied 
 |-  ( ( V < M /\ y = V ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
464 463 adantll 
 |-  ( ( ( ph /\ V < M ) /\ y = V ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
465 270 adantr 
 |-  ( ( ph /\ V < M ) -> V e. ( 0 ... ( N - 1 ) ) )
466 ovexd 
 |-  ( ( ph /\ V < M ) -> ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
467 428 464 465 466 fvmptd 
 |-  ( ( ph /\ V < M ) -> ( F ` V ) = ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) )
468 467 fveq1d 
 |-  ( ( ph /\ V < M ) -> ( ( F ` V ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
469 468 adantr 
 |-  ( ( ( ph /\ V < M ) /\ ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( F ` V ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... V ) ) X. { 1 } ) u. ( ( U " ( ( V + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
470 427 456 469 3eqtr4d 
 |-  ( ( ( ph /\ V < M ) /\ ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) )
471 470 ex 
 |-  ( ( ph /\ V < M ) -> ( ( n e. ( U " ( 1 ... ( V - 1 ) ) ) \/ n e. ( U " ( ( V + 1 ) ... N ) ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
472 341 471 sylbid 
 |-  ( ( ph /\ V < M ) -> ( ( n e. ( U " ( 1 ... N ) ) /\ -. n e. ( U " { V } ) ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
473 472 expdimp 
 |-  ( ( ( ph /\ V < M ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( -. n e. ( U " { V } ) -> ( ( F ` ( V - 1 ) ) ` n ) = ( ( F ` V ) ` n ) ) )
474 473 necon1ad 
 |-  ( ( ( ph /\ V < M ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n e. ( U " { V } ) ) )
475 elimasni 
 |-  ( n e. ( U " { V } ) -> V U n )
476 eqcom 
 |-  ( n = ( U ` V ) <-> ( U ` V ) = n )
477 fnbrfvb 
 |-  ( ( U Fn ( 1 ... N ) /\ V e. ( 1 ... N ) ) -> ( ( U ` V ) = n <-> V U n ) )
478 284 97 477 syl2anc 
 |-  ( ph -> ( ( U ` V ) = n <-> V U n ) )
479 476 478 bitrid 
 |-  ( ph -> ( n = ( U ` V ) <-> V U n ) )
480 475 479 imbitrrid 
 |-  ( ph -> ( n e. ( U " { V } ) -> n = ( U ` V ) ) )
481 480 ad2antrr 
 |-  ( ( ( ph /\ V < M ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( n e. ( U " { V } ) -> n = ( U ` V ) ) )
482 474 481 syld 
 |-  ( ( ( ph /\ V < M ) /\ n e. ( U " ( 1 ... N ) ) ) -> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` V ) ) )
483 482 ralrimiva 
 |-  ( ( ph /\ V < M ) -> A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` V ) ) )
484 fvex 
 |-  ( U ` V ) e. _V
485 eqeq2 
 |-  ( m = ( U ` V ) -> ( n = m <-> n = ( U ` V ) ) )
486 485 imbi2d 
 |-  ( m = ( U ` V ) -> ( ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) <-> ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` V ) ) ) )
487 486 ralbidv 
 |-  ( m = ( U ` V ) -> ( A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) <-> A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` V ) ) ) )
488 484 487 spcev 
 |-  ( A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = ( U ` V ) ) -> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
489 483 488 syl 
 |-  ( ( ph /\ V < M ) -> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
490 eldifsni 
 |-  ( M e. ( ( 0 ... N ) \ { V } ) -> M =/= V )
491 6 490 syl 
 |-  ( ph -> M =/= V )
492 215 30 lttri2d 
 |-  ( ph -> ( M =/= V <-> ( M < V \/ V < M ) ) )
493 491 492 mpbid 
 |-  ( ph -> ( M < V \/ V < M ) )
494 297 489 493 mpjaodan 
 |-  ( ph -> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
495 nfv 
 |-  F/ m ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n )
496 495 rmo2 
 |-  ( E* n e. ( U " ( 1 ... N ) ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) <-> E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) )
497 rmoeq1 
 |-  ( ( U " ( 1 ... N ) ) = ( 1 ... N ) -> ( E* n e. ( U " ( 1 ... N ) ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) <-> E* n e. ( 1 ... N ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) ) )
498 4 101 103 497 4syl 
 |-  ( ph -> ( E* n e. ( U " ( 1 ... N ) ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) <-> E* n e. ( 1 ... N ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) ) )
499 496 498 bitr3id 
 |-  ( ph -> ( E. m A. n e. ( U " ( 1 ... N ) ) ( ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) -> n = m ) <-> E* n e. ( 1 ... N ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) ) )
500 494 499 mpbid 
 |-  ( ph -> E* n e. ( 1 ... N ) ( ( F ` ( V - 1 ) ) ` n ) =/= ( ( F ` V ) ` n ) )