Metamath Proof Explorer

Theorem poimirlem1

Description: Lemma for poimir - the vertices on either side of a skipped vertex differ in at least two dimensions. (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 ) )
poimirlem1.4 
|- ( ph -> M e. ( 1 ... ( N - 1 ) ) )
Assertion poimirlem1 
|- ( ph -> -. E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` 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 poimirlem1.4 
 |-  ( ph -> M e. ( 1 ... ( N - 1 ) ) )
6 f1of 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) --> ( 1 ... N ) )
7 4 6 syl 
 |-  ( ph -> U : ( 1 ... N ) --> ( 1 ... N ) )
8 1 nncnd 
 |-  ( ph -> N e. CC )
9 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
10 8 9 syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
11 1 nnzd 
 |-  ( ph -> N e. ZZ )
12 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
13 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
14 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
15 11 12 13 14 4syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
16 10 15 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
17 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
18 16 17 syl 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
19 18 5 sseldd 
 |-  ( ph -> M e. ( 1 ... N ) )
20 7 19 ffvelcdmd 
 |-  ( ph -> ( U ` M ) e. ( 1 ... N ) )
21 fzp1elp1 
 |-  ( M e. ( 1 ... ( N - 1 ) ) -> ( M + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
22 5 21 syl 
 |-  ( ph -> ( M + 1 ) e. ( 1 ... ( ( N - 1 ) + 1 ) ) )
23 10 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
24 22 23 eleqtrd 
 |-  ( ph -> ( M + 1 ) e. ( 1 ... N ) )
25 7 24 ffvelcdmd 
 |-  ( ph -> ( U ` ( M + 1 ) ) e. ( 1 ... N ) )
26 imassrn 
 |-  ( U " ( M ... ( M + 1 ) ) ) C_ ran U
27 frn 
 |-  ( U : ( 1 ... N ) --> ( 1 ... N ) -> ran U C_ ( 1 ... N ) )
28 4 6 27 3syl 
 |-  ( ph -> ran U C_ ( 1 ... N ) )
29 26 28 sstrid 
 |-  ( ph -> ( U " ( M ... ( M + 1 ) ) ) C_ ( 1 ... N ) )
30 29 sselda 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> n e. ( 1 ... N ) )
31 3 ffvelcdmda 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( T ` n ) e. ZZ )
32 31 zred 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( T ` n ) e. RR )
33 32 ltp1d 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( T ` n ) < ( ( T ` n ) + 1 ) )
34 32 33 ltned 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( T ` n ) =/= ( ( T ` n ) + 1 ) )
35 30 34 syldan 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( T ` n ) =/= ( ( T ` n ) + 1 ) )
36 breq1 
 |-  ( y = ( M - 1 ) -> ( y < M <-> ( M - 1 ) < M ) )
37 id 
 |-  ( y = ( M - 1 ) -> y = ( M - 1 ) )
38 36 37 ifbieq1d 
 |-  ( y = ( M - 1 ) -> if ( y < M , y , ( y + 1 ) ) = if ( ( M - 1 ) < M , ( M - 1 ) , ( y + 1 ) ) )
39 elfzelz 
 |-  ( M e. ( 1 ... ( N - 1 ) ) -> M e. ZZ )
40 5 39 syl 
 |-  ( ph -> M e. ZZ )
41 40 zred 
 |-  ( ph -> M e. RR )
42 41 ltm1d 
 |-  ( ph -> ( M - 1 ) < M )
43 42 iftrued 
 |-  ( ph -> if ( ( M - 1 ) < M , ( M - 1 ) , ( y + 1 ) ) = ( M - 1 ) )
44 38 43 sylan9eqr 
 |-  ( ( ph /\ y = ( M - 1 ) ) -> if ( y < M , y , ( y + 1 ) ) = ( M - 1 ) )
45 44 csbeq1d 
 |-  ( ( ph /\ y = ( M - 1 ) ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( M - 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
46 11 12 syl 
 |-  ( ph -> ( N - 1 ) e. ZZ )
47 elfzm1b 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( M e. ( 1 ... ( N - 1 ) ) <-> ( M - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) ) )
48 40 46 47 syl2anc 
 |-  ( ph -> ( M e. ( 1 ... ( N - 1 ) ) <-> ( M - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) ) )
49 5 48 mpbid 
 |-  ( ph -> ( M - 1 ) e. ( 0 ... ( ( N - 1 ) - 1 ) ) )
50 oveq2 
 |-  ( j = ( M - 1 ) -> ( 1 ... j ) = ( 1 ... ( M - 1 ) ) )
51 50 imaeq2d 
 |-  ( j = ( M - 1 ) -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... ( M - 1 ) ) ) )
52 51 xpeq1d 
 |-  ( j = ( M - 1 ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) )
53 52 adantl 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) )
54 oveq1 
 |-  ( j = ( M - 1 ) -> ( j + 1 ) = ( ( M - 1 ) + 1 ) )
55 40 zcnd 
 |-  ( ph -> M e. CC )
56 npcan1 
 |-  ( M e. CC -> ( ( M - 1 ) + 1 ) = M )
57 55 56 syl 
 |-  ( ph -> ( ( M - 1 ) + 1 ) = M )
58 54 57 sylan9eqr 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( j + 1 ) = M )
59 58 oveq1d 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( ( j + 1 ) ... N ) = ( M ... N ) )
60 59 imaeq2d 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( M ... N ) ) )
61 60 xpeq1d 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( M ... N ) ) X. { 0 } ) )
62 53 61 uneq12d 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) )
63 62 oveq2d 
 |-  ( ( ph /\ j = ( M - 1 ) ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) )
64 49 63 csbied 
 |-  ( ph -> [_ ( M - 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) )
65 64 adantr 
 |-  ( ( ph /\ y = ( M - 1 ) ) -> [_ ( M - 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) )
66 45 65 eqtrd 
 |-  ( ( ph /\ y = ( M - 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 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) )
67 46 zcnd 
 |-  ( ph -> ( N - 1 ) e. CC )
68 npcan1 
 |-  ( ( N - 1 ) e. CC -> ( ( ( N - 1 ) - 1 ) + 1 ) = ( N - 1 ) )
69 67 68 syl 
 |-  ( ph -> ( ( ( N - 1 ) - 1 ) + 1 ) = ( N - 1 ) )
70 peano2zm 
 |-  ( ( N - 1 ) e. ZZ -> ( ( N - 1 ) - 1 ) e. ZZ )
71 uzid 
 |-  ( ( ( N - 1 ) - 1 ) e. ZZ -> ( ( N - 1 ) - 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) )
72 peano2uz 
 |-  ( ( ( N - 1 ) - 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) -> ( ( ( N - 1 ) - 1 ) + 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) )
73 46 70 71 72 4syl 
 |-  ( ph -> ( ( ( N - 1 ) - 1 ) + 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) )
74 69 73 eqeltrrd 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) )
75 fzss2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( ( N - 1 ) - 1 ) ) -> ( 0 ... ( ( N - 1 ) - 1 ) ) C_ ( 0 ... ( N - 1 ) ) )
76 74 75 syl 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) - 1 ) ) C_ ( 0 ... ( N - 1 ) ) )
77 76 49 sseldd 
 |-  ( ph -> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) )
78 ovexd 
 |-  ( ph -> ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) e. _V )
79 2 66 77 78 fvmptd 
 |-  ( ph -> ( F ` ( M - 1 ) ) = ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) )
80 79 fveq1d 
 |-  ( ph -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) ` n ) )
81 80 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) ` n ) )
82 3 ffnd 
 |-  ( ph -> T Fn ( 1 ... N ) )
83 82 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> T Fn ( 1 ... N ) )
84 1ex 
 |-  1 e. _V
85 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M - 1 ) ) ) )
86 84 85 ax-mp 
 |-  ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M - 1 ) ) )
87 c0ex 
 |-  0 e. _V
88 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( M ... N ) ) X. { 0 } ) Fn ( U " ( M ... N ) ) )
89 87 88 ax-mp 
 |-  ( ( U " ( M ... N ) ) X. { 0 } ) Fn ( U " ( M ... N ) )
90 86 89 pm3.2i 
 |-  ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M - 1 ) ) ) /\ ( ( U " ( M ... N ) ) X. { 0 } ) Fn ( U " ( M ... N ) ) )
91 dff1o3 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( U : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' U ) )
92 91 simprbi 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' U )
93 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) )
94 4 92 93 3syl 
 |-  ( ph -> ( U " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) )
95 fzdisj 
 |-  ( ( M - 1 ) < M -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) = (/) )
96 42 95 syl 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) = (/) )
97 96 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( U " (/) ) )
98 ima0 
 |-  ( U " (/) ) = (/)
99 97 98 eqtrdi 
 |-  ( ph -> ( U " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = (/) )
100 94 99 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) = (/) )
101 fnun 
 |-  ( ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M - 1 ) ) ) /\ ( ( U " ( M ... N ) ) X. { 0 } ) Fn ( U " ( M ... N ) ) ) /\ ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) ) )
102 90 100 101 sylancr 
 |-  ( ph -> ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) ) )
103 elfzuz 
 |-  ( M e. ( 1 ... ( N - 1 ) ) -> M e. ( ZZ>= ` 1 ) )
104 5 103 syl 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
105 57 104 eqeltrd 
 |-  ( ph -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
106 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
107 uzid 
 |-  ( ( M - 1 ) e. ZZ -> ( M - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
108 peano2uz 
 |-  ( ( M - 1 ) e. ( ZZ>= ` ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
109 40 106 107 108 4syl 
 |-  ( ph -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
110 57 109 eqeltrrd 
 |-  ( ph -> M e. ( ZZ>= ` ( M - 1 ) ) )
111 peano2uz 
 |-  ( M e. ( ZZ>= ` ( M - 1 ) ) -> ( M + 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
112 uzss 
 |-  ( ( M + 1 ) e. ( ZZ>= ` ( M - 1 ) ) -> ( ZZ>= ` ( M + 1 ) ) C_ ( ZZ>= ` ( M - 1 ) ) )
113 110 111 112 3syl 
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ ( ZZ>= ` ( M - 1 ) ) )
114 elfzuz3 
 |-  ( M e. ( 1 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
115 eluzp1p1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
116 5 114 115 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )
117 10 116 eqeltrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
118 113 117 sseldd 
 |-  ( ph -> N e. ( ZZ>= ` ( M - 1 ) ) )
119 fzsplit2 
 |-  ( ( ( ( M - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( M - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) )
120 105 118 119 syl2anc 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) )
121 57 oveq1d 
 |-  ( ph -> ( ( ( M - 1 ) + 1 ) ... N ) = ( M ... N ) )
122 121 uneq2d 
 |-  ( ph -> ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) )
123 120 122 eqtrd 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) )
124 123 imaeq2d 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) ) )
125 imaundi 
 |-  ( U " ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) ) = ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) )
126 124 125 eqtrdi 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) ) )
127 f1ofo 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -onto-> ( 1 ... N ) )
128 foima 
 |-  ( U : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
129 4 127 128 3syl 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( 1 ... N ) )
130 126 129 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) ) = ( 1 ... N ) )
131 130 fneq2d 
 |-  ( ph -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M - 1 ) ) ) u. ( U " ( M ... N ) ) ) <-> ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
132 102 131 mpbid 
 |-  ( ph -> ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
133 132 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
134 ovexd 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( 1 ... N ) e. _V )
135 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
136 eqidd 
 |-  ( ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( T ` n ) = ( T ` n ) )
137 100 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) = (/) )
138 fzss2 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( M ... ( M + 1 ) ) C_ ( M ... N ) )
139 imass2 
 |-  ( ( M ... ( M + 1 ) ) C_ ( M ... N ) -> ( U " ( M ... ( M + 1 ) ) ) C_ ( U " ( M ... N ) ) )
140 117 138 139 3syl 
 |-  ( ph -> ( U " ( M ... ( M + 1 ) ) ) C_ ( U " ( M ... N ) ) )
141 140 sselda 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> n e. ( U " ( M ... N ) ) )
142 fvun2 
 |-  ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M - 1 ) ) ) /\ ( ( U " ( M ... N ) ) X. { 0 } ) Fn ( U " ( M ... N ) ) /\ ( ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) = (/) /\ n e. ( U " ( M ... N ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( M ... N ) ) X. { 0 } ) ` n ) )
143 86 89 142 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) i^i ( U " ( M ... N ) ) ) = (/) /\ n e. ( U " ( M ... N ) ) ) -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( M ... N ) ) X. { 0 } ) ` n ) )
144 137 141 143 syl2anc 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( M ... N ) ) X. { 0 } ) ` n ) )
145 87 fvconst2 
 |-  ( n e. ( U " ( M ... N ) ) -> ( ( ( U " ( M ... N ) ) X. { 0 } ) ` n ) = 0 )
146 141 145 syl 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( U " ( M ... N ) ) X. { 0 } ) ` n ) = 0 )
147 144 146 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ` n ) = 0 )
148 147 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ` n ) = 0 )
149 83 133 134 134 135 136 148 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
150 30 149 mpdan 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( U " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 0 ) )
151 31 zcnd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( T ` n ) e. CC )
152 151 addridd 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( T ` n ) + 0 ) = ( T ` n ) )
153 30 152 syldan 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( T ` n ) + 0 ) = ( T ` n ) )
154 81 150 153 3eqtrd 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( T ` n ) )
155 breq1 
 |-  ( y = M -> ( y < M <-> M < M ) )
156 oveq1 
 |-  ( y = M -> ( y + 1 ) = ( M + 1 ) )
157 155 156 ifbieq2d 
 |-  ( y = M -> if ( y < M , y , ( y + 1 ) ) = if ( M < M , y , ( M + 1 ) ) )
158 41 ltnrd 
 |-  ( ph -> -. M < M )
159 158 iffalsed 
 |-  ( ph -> if ( M < M , y , ( M + 1 ) ) = ( M + 1 ) )
160 157 159 sylan9eqr 
 |-  ( ( ph /\ y = M ) -> if ( y < M , y , ( y + 1 ) ) = ( M + 1 ) )
161 160 csbeq1d 
 |-  ( ( ph /\ y = M ) -> [_ if ( y < M , y , ( y + 1 ) ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( M + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
162 ovex 
 |-  ( M + 1 ) e. _V
163 oveq2 
 |-  ( j = ( M + 1 ) -> ( 1 ... j ) = ( 1 ... ( M + 1 ) ) )
164 163 imaeq2d 
 |-  ( j = ( M + 1 ) -> ( U " ( 1 ... j ) ) = ( U " ( 1 ... ( M + 1 ) ) ) )
165 164 xpeq1d 
 |-  ( j = ( M + 1 ) -> ( ( U " ( 1 ... j ) ) X. { 1 } ) = ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) )
166 oveq1 
 |-  ( j = ( M + 1 ) -> ( j + 1 ) = ( ( M + 1 ) + 1 ) )
167 166 oveq1d 
 |-  ( j = ( M + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( M + 1 ) + 1 ) ... N ) )
168 167 imaeq2d 
 |-  ( j = ( M + 1 ) -> ( U " ( ( j + 1 ) ... N ) ) = ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) )
169 168 xpeq1d 
 |-  ( j = ( M + 1 ) -> ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
170 165 169 uneq12d 
 |-  ( j = ( M + 1 ) -> ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
171 170 oveq2d 
 |-  ( j = ( M + 1 ) -> ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
172 162 171 csbie 
 |-  [_ ( M + 1 ) / j ]_ ( T oF + ( ( ( U " ( 1 ... j ) ) X. { 1 } ) u. ( ( U " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
173 161 172 eqtrdi 
 |-  ( ( ph /\ y = M ) -> [_ 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 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
174 fz1ssfz0 
 |-  ( 1 ... ( N - 1 ) ) C_ ( 0 ... ( N - 1 ) )
175 174 5 sselid 
 |-  ( ph -> M e. ( 0 ... ( N - 1 ) ) )
176 ovexd 
 |-  ( ph -> ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
177 2 173 175 176 fvmptd 
 |-  ( ph -> ( F ` M ) = ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
178 177 fveq1d 
 |-  ( ph -> ( ( F ` M ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
179 178 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( F ` M ) ` n ) = ( ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
180 fnconstg 
 |-  ( 1 e. _V -> ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M + 1 ) ) ) )
181 84 180 ax-mp 
 |-  ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M + 1 ) ) )
182 fnconstg 
 |-  ( 0 e. _V -> ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) )
183 87 182 ax-mp 
 |-  ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( M + 1 ) + 1 ) ... N ) )
184 181 183 pm3.2i 
 |-  ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M + 1 ) ) ) /\ ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) )
185 imain 
 |-  ( Fun `' U -> ( U " ( ( 1 ... ( M + 1 ) ) i^i ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
186 4 92 185 3syl 
 |-  ( ph -> ( U " ( ( 1 ... ( M + 1 ) ) i^i ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
187 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
188 41 187 syl 
 |-  ( ph -> ( M + 1 ) e. RR )
189 188 ltp1d 
 |-  ( ph -> ( M + 1 ) < ( ( M + 1 ) + 1 ) )
190 fzdisj 
 |-  ( ( M + 1 ) < ( ( M + 1 ) + 1 ) -> ( ( 1 ... ( M + 1 ) ) i^i ( ( ( M + 1 ) + 1 ) ... N ) ) = (/) )
191 189 190 syl 
 |-  ( ph -> ( ( 1 ... ( M + 1 ) ) i^i ( ( ( M + 1 ) + 1 ) ... N ) ) = (/) )
192 191 imaeq2d 
 |-  ( ph -> ( U " ( ( 1 ... ( M + 1 ) ) i^i ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( U " (/) ) )
193 186 192 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( U " (/) ) )
194 193 98 eqtrdi 
 |-  ( ph -> ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = (/) )
195 fnun 
 |-  ( ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M + 1 ) ) ) /\ ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) /\ ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = (/) ) -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
196 184 194 195 sylancr 
 |-  ( ph -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
197 fzsplit 
 |-  ( ( M + 1 ) e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
198 24 197 syl 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) )
199 198 imaeq2d 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( U " ( ( 1 ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
200 imaundi 
 |-  ( U " ( ( 1 ... ( M + 1 ) ) u. ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) )
201 199 200 eqtrdi 
 |-  ( ph -> ( U " ( 1 ... N ) ) = ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) )
202 201 129 eqtr3d 
 |-  ( ph -> ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
203 202 fneq2d 
 |-  ( ph -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( U " ( 1 ... ( M + 1 ) ) ) u. ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) <-> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
204 196 203 mpbid 
 |-  ( ph -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
205 204 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
206 194 adantr 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = (/) )
207 fzss1 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( M ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) )
208 imass2 
 |-  ( ( M ... ( M + 1 ) ) C_ ( 1 ... ( M + 1 ) ) -> ( U " ( M ... ( M + 1 ) ) ) C_ ( U " ( 1 ... ( M + 1 ) ) ) )
209 104 207 208 3syl 
 |-  ( ph -> ( U " ( M ... ( M + 1 ) ) ) C_ ( U " ( 1 ... ( M + 1 ) ) ) )
210 209 sselda 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> n e. ( U " ( 1 ... ( M + 1 ) ) ) )
211 fvun1 
 |-  ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) Fn ( U " ( 1 ... ( M + 1 ) ) ) /\ ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) /\ ( ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( M + 1 ) ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) ` n ) )
212 181 183 211 mp3an12 
 |-  ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) i^i ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) ) = (/) /\ n e. ( U " ( 1 ... ( M + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) ` n ) )
213 206 210 212 syl2anc 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) ` n ) )
214 84 fvconst2 
 |-  ( n e. ( U " ( 1 ... ( M + 1 ) ) ) -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) ` n ) = 1 )
215 210 214 syl 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) ` n ) = 1 )
216 213 215 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
217 216 adantr 
 |-  ( ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = 1 )
218 83 205 134 134 135 136 217 ofval 
 |-  ( ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
219 30 218 mpdan 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( T oF + ( ( ( U " ( 1 ... ( M + 1 ) ) ) X. { 1 } ) u. ( ( U " ( ( ( M + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( T ` n ) + 1 ) )
220 179 219 eqtrd 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( F ` M ) ` n ) = ( ( T ` n ) + 1 ) )
221 35 154 220 3netr4d 
 |-  ( ( ph /\ n e. ( U " ( M ... ( M + 1 ) ) ) ) -> ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )
222 221 ralrimiva 
 |-  ( ph -> A. n e. ( U " ( M ... ( M + 1 ) ) ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )
223 fzpr 
 |-  ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
224 5 39 223 3syl 
 |-  ( ph -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } )
225 224 imaeq2d 
 |-  ( ph -> ( U " ( M ... ( M + 1 ) ) ) = ( U " { M , ( M + 1 ) } ) )
226 f1ofn 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U Fn ( 1 ... N ) )
227 4 226 syl 
 |-  ( ph -> U Fn ( 1 ... N ) )
228 fnimapr 
 |-  ( ( U Fn ( 1 ... N ) /\ M e. ( 1 ... N ) /\ ( M + 1 ) e. ( 1 ... N ) ) -> ( U " { M , ( M + 1 ) } ) = { ( U ` M ) , ( U ` ( M + 1 ) ) } )
229 227 19 24 228 syl3anc 
 |-  ( ph -> ( U " { M , ( M + 1 ) } ) = { ( U ` M ) , ( U ` ( M + 1 ) ) } )
230 225 229 eqtrd 
 |-  ( ph -> ( U " ( M ... ( M + 1 ) ) ) = { ( U ` M ) , ( U ` ( M + 1 ) ) } )
231 222 230 raleqtrdv 
 |-  ( ph -> A. n e. { ( U ` M ) , ( U ` ( M + 1 ) ) } ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )
232 fvex 
 |-  ( U ` M ) e. _V
233 fvex 
 |-  ( U ` ( M + 1 ) ) e. _V
234 fveq2 
 |-  ( n = ( U ` M ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) )
235 fveq2 
 |-  ( n = ( U ` M ) -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` ( U ` M ) ) )
236 234 235 neeq12d 
 |-  ( n = ( U ` M ) -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) ) )
237 fveq2 
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) )
238 fveq2 
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) )
239 237 238 neeq12d 
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
240 232 233 236 239 ralpr 
 |-  ( A. n e. { ( U ` M ) , ( U ` ( M + 1 ) ) } ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
241 231 240 sylib 
 |-  ( ph -> ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
242 41 ltp1d 
 |-  ( ph -> M < ( M + 1 ) )
243 41 242 ltned 
 |-  ( ph -> M =/= ( M + 1 ) )
244 f1of1 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -1-1-> ( 1 ... N ) )
245 4 244 syl 
 |-  ( ph -> U : ( 1 ... N ) -1-1-> ( 1 ... N ) )
246 f1veqaeq 
 |-  ( ( U : ( 1 ... N ) -1-1-> ( 1 ... N ) /\ ( M e. ( 1 ... N ) /\ ( M + 1 ) e. ( 1 ... N ) ) ) -> ( ( U ` M ) = ( U ` ( M + 1 ) ) -> M = ( M + 1 ) ) )
247 245 19 24 246 syl12anc 
 |-  ( ph -> ( ( U ` M ) = ( U ` ( M + 1 ) ) -> M = ( M + 1 ) ) )
248 247 necon3d 
 |-  ( ph -> ( M =/= ( M + 1 ) -> ( U ` M ) =/= ( U ` ( M + 1 ) ) ) )
249 243 248 mpd 
 |-  ( ph -> ( U ` M ) =/= ( U ` ( M + 1 ) ) )
250 236 anbi1d 
 |-  ( n = ( U ` M ) -> ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) <-> ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) ) )
251 neeq1 
 |-  ( n = ( U ` M ) -> ( n =/= m <-> ( U ` M ) =/= m ) )
252 250 251 anbi12d 
 |-  ( n = ( U ` M ) -> ( ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> ( ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ ( U ` M ) =/= m ) ) )
253 fveq2 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( F ` ( M - 1 ) ) ` m ) = ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) )
254 fveq2 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( F ` M ) ` m ) = ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) )
255 253 254 neeq12d 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
256 255 anbi2d 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) <-> ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) ) )
257 neeq2 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( U ` M ) =/= m <-> ( U ` M ) =/= ( U ` ( M + 1 ) ) ) )
258 256 257 anbi12d 
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ ( U ` M ) =/= m ) <-> ( ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) /\ ( U ` M ) =/= ( U ` ( M + 1 ) ) ) ) )
259 252 258 rspc2ev 
 |-  ( ( ( U ` M ) e. ( 1 ... N ) /\ ( U ` ( M + 1 ) ) e. ( 1 ... N ) /\ ( ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) /\ ( U ` M ) =/= ( U ` ( M + 1 ) ) ) ) -> E. n e. ( 1 ... N ) E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
260 20 25 241 249 259 syl112anc 
 |-  ( ph -> E. n e. ( 1 ... N ) E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
261 dfrex2 
 |-  ( E. n e. ( 1 ... N ) E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> -. A. n e. ( 1 ... N ) -. E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
262 fveq2 
 |-  ( n = m -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` m ) )
263 fveq2 
 |-  ( n = m -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` m ) )
264 262 263 neeq12d 
 |-  ( n = m -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) )
265 264 rmo4 
 |-  ( E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> A. n e. ( 1 ... N ) A. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) )
266 dfral2 
 |-  ( A. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) <-> -. E. m e. ( 1 ... N ) -. ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) )
267 df-ne 
 |-  ( n =/= m <-> -. n = m )
268 267 anbi2i 
 |-  ( ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ -. n = m ) )
269 annim 
 |-  ( ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ -. n = m ) <-> -. ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) )
270 268 269 bitri 
 |-  ( ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> -. ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) )
271 270 rexbii 
 |-  ( E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> E. m e. ( 1 ... N ) -. ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) )
272 266 271 xchbinxr 
 |-  ( A. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) <-> -. E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
273 272 ralbii 
 |-  ( A. n e. ( 1 ... N ) A. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) -> n = m ) <-> A. n e. ( 1 ... N ) -. E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
274 265 273 bitri 
 |-  ( E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> A. n e. ( 1 ... N ) -. E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) )
275 261 274 xchbinxr 
 |-  ( E. n e. ( 1 ... N ) E. m e. ( 1 ... N ) ( ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) /\ ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) /\ n =/= m ) <-> -. E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )
276 260 275 sylib 
 |-  ( ph -> -. E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )