Metamath Proof Explorer


Theorem seqf1olem1

Description: Lemma for seqf1o . (Contributed by Mario Carneiro, 26-Feb-2014) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses seqf1o.1
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqf1o.2
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
seqf1o.3
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqf1o.4
|- ( ph -> N e. ( ZZ>= ` M ) )
seqf1o.5
|- ( ph -> C C_ S )
seqf1olem.5
|- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
seqf1olem.6
|- ( ph -> G : ( M ... ( N + 1 ) ) --> C )
seqf1olem.7
|- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
seqf1olem.8
|- K = ( `' F ` ( N + 1 ) )
Assertion seqf1olem1
|- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqf1o.2
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqf1o.3
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqf1o.4
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqf1o.5
 |-  ( ph -> C C_ S )
6 seqf1olem.5
 |-  ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
7 seqf1olem.6
 |-  ( ph -> G : ( M ... ( N + 1 ) ) --> C )
8 seqf1olem.7
 |-  J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
9 seqf1olem.8
 |-  K = ( `' F ` ( N + 1 ) )
10 fvexd
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) e. _V )
11 fvex
 |-  ( `' F ` x ) e. _V
12 ovex
 |-  ( ( `' F ` x ) - 1 ) e. _V
13 11 12 ifex
 |-  if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V
14 13 a1i
 |-  ( ( ph /\ x e. ( M ... N ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V )
15 iftrue
 |-  ( k < K -> if ( k < K , k , ( k + 1 ) ) = k )
16 15 fveq2d
 |-  ( k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
17 16 eqeq2d
 |-  ( k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
18 17 adantl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
19 simprr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x = ( F ` k ) )
20 elfzelz
 |-  ( k e. ( M ... N ) -> k e. ZZ )
21 20 zred
 |-  ( k e. ( M ... N ) -> k e. RR )
22 21 ad2antlr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. RR )
23 simprl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k < K )
24 22 23 gtned
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> K =/= k )
25 f1of
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
26 6 25 syl
 |-  ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
27 26 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
28 fzssp1
 |-  ( M ... N ) C_ ( M ... ( N + 1 ) )
29 simplr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... N ) )
30 28 29 sselid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... ( N + 1 ) ) )
31 27 30 ffvelrnd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... ( N + 1 ) ) )
32 elfzp1
 |-  ( N e. ( ZZ>= ` M ) -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
33 4 32 syl
 |-  ( ph -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
34 33 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
35 31 34 mpbid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) )
36 35 ord
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> ( F ` k ) = ( N + 1 ) ) )
37 6 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
38 f1ocnvfv
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
39 37 30 38 syl2anc
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
40 9 eqeq1i
 |-  ( K = k <-> ( `' F ` ( N + 1 ) ) = k )
41 39 40 syl6ibr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> K = k ) )
42 36 41 syld
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> K = k ) )
43 42 necon1ad
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( K =/= k -> ( F ` k ) e. ( M ... N ) ) )
44 24 43 mpd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... N ) )
45 19 44 eqeltrd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x e. ( M ... N ) )
46 19 eqcomd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) = x )
47 f1ocnvfv
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
48 37 30 47 syl2anc
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
49 46 48 mpd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) = k )
50 49 23 eqbrtrd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) < K )
51 iftrue
 |-  ( ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
52 50 51 syl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
53 52 49 eqtr2d
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
54 45 53 jca
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) )
55 54 expr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` k ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
56 18 55 sylbid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
57 iffalse
 |-  ( -. k < K -> if ( k < K , k , ( k + 1 ) ) = ( k + 1 ) )
58 57 fveq2d
 |-  ( -. k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
59 58 eqeq2d
 |-  ( -. k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
60 59 adantl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
61 simprr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x = ( F ` ( k + 1 ) ) )
62 f1ocnv
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
63 6 62 syl
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
64 f1of1
 |-  ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
65 63 64 syl
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
66 f1f
 |-  ( `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
67 65 66 syl
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
68 peano2uz
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
69 4 68 syl
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
70 eluzfz2
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
71 69 70 syl
 |-  ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
72 67 71 ffvelrnd
 |-  ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
73 9 72 eqeltrid
 |-  ( ph -> K e. ( M ... ( N + 1 ) ) )
74 73 elfzelzd
 |-  ( ph -> K e. ZZ )
75 74 zred
 |-  ( ph -> K e. RR )
76 75 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K e. RR )
77 21 ad2antlr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. RR )
78 peano2re
 |-  ( k e. RR -> ( k + 1 ) e. RR )
79 77 78 syl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. RR )
80 simprl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. k < K )
81 76 77 80 nltled
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K <_ k )
82 77 ltp1d
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k < ( k + 1 ) )
83 76 77 79 81 82 lelttrd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K < ( k + 1 ) )
84 76 83 ltned
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K =/= ( k + 1 ) )
85 26 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
86 fzp1elp1
 |-  ( k e. ( M ... N ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
87 86 ad2antlr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
88 85 87 ffvelrnd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) )
89 elfzp1
 |-  ( N e. ( ZZ>= ` M ) -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
90 4 89 syl
 |-  ( ph -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
91 90 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
92 88 91 mpbid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
93 92 ord
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
94 6 ad2antrr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
95 f1ocnvfv
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( k + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = ( k + 1 ) ) )
96 94 87 95 syl2anc
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = ( k + 1 ) ) )
97 9 eqeq1i
 |-  ( K = ( k + 1 ) <-> ( `' F ` ( N + 1 ) ) = ( k + 1 ) )
98 96 97 syl6ibr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> K = ( k + 1 ) ) )
99 93 98 syld
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> K = ( k + 1 ) ) )
100 99 necon1ad
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( K =/= ( k + 1 ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) ) )
101 84 100 mpd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) )
102 61 101 eqeltrd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x e. ( M ... N ) )
103 61 eqcomd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) = x )
104 f1ocnvfv
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( k + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
105 94 87 104 syl2anc
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
106 103 105 mpd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( `' F ` x ) = ( k + 1 ) )
107 106 breq1d
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K <-> ( k + 1 ) < K ) )
108 lttr
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR /\ K e. RR ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
109 77 79 76 108 syl3anc
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
110 82 109 mpand
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) < K -> k < K ) )
111 107 110 sylbid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K -> k < K ) )
112 80 111 mtod
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. ( `' F ` x ) < K )
113 iffalse
 |-  ( -. ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
114 112 113 syl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
115 106 oveq1d
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) - 1 ) = ( ( k + 1 ) - 1 ) )
116 77 recnd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. CC )
117 ax-1cn
 |-  1 e. CC
118 pncan
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
119 116 117 118 sylancl
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) - 1 ) = k )
120 114 115 119 3eqtrrd
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
121 102 120 jca
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) )
122 121 expr
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` ( k + 1 ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
123 60 122 sylbid
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
124 56 123 pm2.61dan
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
125 124 expimpd
 |-  ( ph -> ( ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
126 51 eqeq2d
 |-  ( ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
127 126 adantl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
128 eluzel2
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
129 4 128 syl
 |-  ( ph -> M e. ZZ )
130 129 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M e. ZZ )
131 eluzelz
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
132 4 131 syl
 |-  ( ph -> N e. ZZ )
133 132 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> N e. ZZ )
134 simprr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k = ( `' F ` x ) )
135 67 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
136 simplr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... N ) )
137 28 136 sselid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... ( N + 1 ) ) )
138 135 137 ffvelrnd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
139 134 138 eqeltrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... ( N + 1 ) ) )
140 139 elfzelzd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ZZ )
141 elfzle1
 |-  ( k e. ( M ... ( N + 1 ) ) -> M <_ k )
142 139 141 syl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M <_ k )
143 140 zred
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. RR )
144 75 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K e. RR )
145 132 peano2zd
 |-  ( ph -> ( N + 1 ) e. ZZ )
146 145 zred
 |-  ( ph -> ( N + 1 ) e. RR )
147 146 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( N + 1 ) e. RR )
148 simprl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) < K )
149 134 148 eqbrtrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < K )
150 elfzle2
 |-  ( K e. ( M ... ( N + 1 ) ) -> K <_ ( N + 1 ) )
151 73 150 syl
 |-  ( ph -> K <_ ( N + 1 ) )
152 151 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K <_ ( N + 1 ) )
153 143 144 147 149 152 ltletrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < ( N + 1 ) )
154 zleltp1
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k <_ N <-> k < ( N + 1 ) ) )
155 140 133 154 syl2anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k <_ N <-> k < ( N + 1 ) ) )
156 153 155 mpbird
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k <_ N )
157 130 133 140 142 156 elfzd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... N ) )
158 149 16 syl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
159 134 fveq2d
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` k ) = ( F ` ( `' F ` x ) ) )
160 6 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
161 f1ocnvfv2
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
162 160 137 161 syl2anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` ( `' F ` x ) ) = x )
163 158 159 162 3eqtrrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
164 157 163 jca
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) )
165 164 expr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = ( `' F ` x ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
166 127 165 sylbid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
167 113 eqeq2d
 |-  ( -. ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
168 167 adantl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
169 129 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. ZZ )
170 132 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. ZZ )
171 simprr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k = ( ( `' F ` x ) - 1 ) )
172 67 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
173 simplr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... N ) )
174 28 173 sselid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
175 172 174 ffvelrnd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
176 175 elfzelzd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ZZ )
177 peano2zm
 |-  ( ( `' F ` x ) e. ZZ -> ( ( `' F ` x ) - 1 ) e. ZZ )
178 176 177 syl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) e. ZZ )
179 171 178 eqeltrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ZZ )
180 129 zred
 |-  ( ph -> M e. RR )
181 180 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. RR )
182 75 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. RR )
183 179 zred
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. RR )
184 elfzle1
 |-  ( K e. ( M ... ( N + 1 ) ) -> M <_ K )
185 73 184 syl
 |-  ( ph -> M <_ K )
186 185 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ K )
187 176 zred
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. RR )
188 simprl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. ( `' F ` x ) < K )
189 182 187 188 nltled
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( `' F ` x ) )
190 elfzelz
 |-  ( x e. ( M ... N ) -> x e. ZZ )
191 190 adantl
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. ZZ )
192 191 zred
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
193 132 zred
 |-  ( ph -> N e. RR )
194 193 adantr
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
195 146 adantr
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
196 elfzle2
 |-  ( x e. ( M ... N ) -> x <_ N )
197 196 adantl
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
198 194 ltp1d
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
199 192 194 195 197 198 lelttrd
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
200 192 199 gtned
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) =/= x )
201 200 adantr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) =/= x )
202 65 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
203 71 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
204 f1fveq
 |-  ( ( `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) /\ ( ( N + 1 ) e. ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) ) -> ( ( `' F ` ( N + 1 ) ) = ( `' F ` x ) <-> ( N + 1 ) = x ) )
205 202 203 174 204 syl12anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) = ( `' F ` x ) <-> ( N + 1 ) = x ) )
206 205 necon3bid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) <-> ( N + 1 ) =/= x ) )
207 201 206 mpbird
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
208 9 neeq1i
 |-  ( K =/= ( `' F ` x ) <-> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
209 207 208 sylibr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K =/= ( `' F ` x ) )
210 209 necomd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) =/= K )
211 182 187 189 210 leneltd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K < ( `' F ` x ) )
212 74 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. ZZ )
213 zltlem1
 |-  ( ( K e. ZZ /\ ( `' F ` x ) e. ZZ ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
214 212 176 213 syl2anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
215 211 214 mpbid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( ( `' F ` x ) - 1 ) )
216 215 171 breqtrrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ k )
217 181 182 183 186 216 letrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ k )
218 elfzle2
 |-  ( ( `' F ` x ) e. ( M ... ( N + 1 ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
219 175 218 syl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
220 193 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. RR )
221 1re
 |-  1 e. RR
222 lesubadd
 |-  ( ( ( `' F ` x ) e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
223 221 222 mp3an2
 |-  ( ( ( `' F ` x ) e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
224 187 220 223 syl2anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
225 219 224 mpbird
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) <_ N )
226 171 225 eqbrtrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k <_ N )
227 169 170 179 217 226 elfzd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ( M ... N ) )
228 182 183 216 lensymd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. k < K )
229 228 58 syl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
230 171 oveq1d
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( ( ( `' F ` x ) - 1 ) + 1 ) )
231 176 zcnd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. CC )
232 npcan
 |-  ( ( ( `' F ` x ) e. CC /\ 1 e. CC ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
233 231 117 232 sylancl
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
234 230 233 eqtrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( `' F ` x ) )
235 234 fveq2d
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( k + 1 ) ) = ( F ` ( `' F ` x ) ) )
236 6 ad2antrr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
237 236 174 161 syl2anc
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
238 229 235 237 3eqtrrd
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
239 227 238 jca
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) )
240 239 expr
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = ( ( `' F ` x ) - 1 ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
241 168 240 sylbid
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
242 166 241 pm2.61dan
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
243 242 expimpd
 |-  ( ph -> ( ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
244 125 243 impbid
 |-  ( ph -> ( ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) <-> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
245 8 10 14 244 f1od
 |-  ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )