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