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