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 ffvelrnd
 |-  ( 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 ffvelrnd
 |-  ( 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 ffvelrnda
 |-  ( ( 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 addid1d
 |-  ( ( 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 230 raleqdv
 |-  ( ph -> ( A. n e. ( U " ( M ... ( M + 1 ) ) ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> A. n e. { ( U ` M ) , ( U ` ( M + 1 ) ) } ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) ) )
232 222 231 mpbid
 |-  ( ph -> A. n e. { ( U ` M ) , ( U ` ( M + 1 ) ) } ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )
233 fvex
 |-  ( U ` M ) e. _V
234 fvex
 |-  ( U ` ( M + 1 ) ) e. _V
235 fveq2
 |-  ( n = ( U ` M ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) )
236 fveq2
 |-  ( n = ( U ` M ) -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` ( U ` M ) ) )
237 235 236 neeq12d
 |-  ( n = ( U ` M ) -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) ) )
238 fveq2
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) )
239 fveq2
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) )
240 238 239 neeq12d
 |-  ( n = ( U ` ( M + 1 ) ) -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
241 233 234 237 240 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 ) ) ) ) )
242 232 241 sylib
 |-  ( ph -> ( ( ( F ` ( M - 1 ) ) ` ( U ` M ) ) =/= ( ( F ` M ) ` ( U ` M ) ) /\ ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
243 41 ltp1d
 |-  ( ph -> M < ( M + 1 ) )
244 41 243 ltned
 |-  ( ph -> M =/= ( M + 1 ) )
245 f1of1
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U : ( 1 ... N ) -1-1-> ( 1 ... N ) )
246 4 245 syl
 |-  ( ph -> U : ( 1 ... N ) -1-1-> ( 1 ... N ) )
247 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 ) ) )
248 246 19 24 247 syl12anc
 |-  ( ph -> ( ( U ` M ) = ( U ` ( M + 1 ) ) -> M = ( M + 1 ) ) )
249 248 necon3d
 |-  ( ph -> ( M =/= ( M + 1 ) -> ( U ` M ) =/= ( U ` ( M + 1 ) ) ) )
250 244 249 mpd
 |-  ( ph -> ( U ` M ) =/= ( U ` ( M + 1 ) ) )
251 237 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 ) ) ) )
252 neeq1
 |-  ( n = ( U ` M ) -> ( n =/= m <-> ( U ` M ) =/= m ) )
253 251 252 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 ) ) )
254 fveq2
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( F ` ( M - 1 ) ) ` m ) = ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) )
255 fveq2
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( F ` M ) ` m ) = ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) )
256 254 255 neeq12d
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) <-> ( ( F ` ( M - 1 ) ) ` ( U ` ( M + 1 ) ) ) =/= ( ( F ` M ) ` ( U ` ( M + 1 ) ) ) ) )
257 256 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 ) ) ) ) ) )
258 neeq2
 |-  ( m = ( U ` ( M + 1 ) ) -> ( ( U ` M ) =/= m <-> ( U ` M ) =/= ( U ` ( M + 1 ) ) ) )
259 257 258 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 ) ) ) ) )
260 253 259 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 ) )
261 20 25 242 250 260 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 ) )
262 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 ) )
263 fveq2
 |-  ( n = m -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` m ) )
264 fveq2
 |-  ( n = m -> ( ( F ` M ) ` n ) = ( ( F ` M ) ` m ) )
265 263 264 neeq12d
 |-  ( n = m -> ( ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) <-> ( ( F ` ( M - 1 ) ) ` m ) =/= ( ( F ` M ) ` m ) ) )
266 265 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 ) )
267 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 ) )
268 df-ne
 |-  ( n =/= m <-> -. n = m )
269 268 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 ) )
270 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 ) )
271 269 270 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 ) )
272 271 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 ) )
273 267 272 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 ) )
274 273 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 ) )
275 266 274 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 ) )
276 262 275 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 ) )
277 261 276 sylib
 |-  ( ph -> -. E* n e. ( 1 ... N ) ( ( F ` ( M - 1 ) ) ` n ) =/= ( ( F ` M ) ` n ) )