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 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
seqf1o.2 ( ( 𝜑 ∧ ( 𝑥𝐶𝑦𝐶 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
seqf1o.3 ( ( 𝜑 ∧ ( 𝑥𝑆𝑦𝑆𝑧𝑆 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
seqf1o.4 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqf1o.5 ( 𝜑𝐶𝑆 )
seqf1olem.5 ( 𝜑𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
seqf1olem.6 ( 𝜑𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
seqf1olem.7 𝐽 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) ) )
seqf1olem.8 𝐾 = ( 𝐹 ‘ ( 𝑁 + 1 ) )
Assertion seqf1olem1 ( 𝜑𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )

Proof

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