Metamath Proof Explorer

Theorem metakunt1

Description: A is an endomapping. (Contributed by metakunt, 23-May-2024)

Ref Expression
Hypotheses metakunt1.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt1.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt1.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt1.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
Assertion metakunt1 ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )

Proof

Step Hyp Ref Expression
1 metakunt1.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt1.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt1.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt1.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 eleq1 ⊢ ( 𝑀 = if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) → ( 𝑀 ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ∈ ( 1 ... 𝑀 ) ) )
6 eleq1 ⊢ ( if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) → ( if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ∈ ( 1 ... 𝑀 ) ) )
7 1zzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 1 ∈ ℤ )
8 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 𝑀 ∈ ℤ )
10 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 𝑀 ∈ ℕ )
11 10 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 1 ≤ 𝑀 )
12 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 𝑀 ∈ ℝ )
14 13 leidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 𝑀 ≤ 𝑀 )
15 7 9 9 11 14 elfzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑥 = 𝐼 ) → 𝑀 ∈ ( 1 ... 𝑀 ) )
16 eleq1 ⊢ ( 𝑥 = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) → ( 𝑥 ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ∈ ( 1 ... 𝑀 ) ) )
17 eleq1 ⊢ ( ( 𝑥 − 1 ) = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) → ( ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) ↔ if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ∈ ( 1 ... 𝑀 ) ) )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝐼 ) ∧ 𝑥 < 𝐼 ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
19 pm4.56 ⊢ ( ( ¬ 𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼 ) ↔ ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) )
20 19 anbi2i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) ) )
21 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝐼 ∈ ℝ )
23 elfznn ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℕ )
24 23 nnred ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ∈ ℝ )
25 24 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ∈ ℝ )
26 22 25 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝐼 ∈ ℝ ∧ 𝑥 ∈ ℝ ) )
27 axlttri ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐼 < 𝑥 ↔ ¬ ( 𝐼 = 𝑥 ∨ 𝑥 < 𝐼 ) ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝐼 < 𝑥 ↔ ¬ ( 𝐼 = 𝑥 ∨ 𝑥 < 𝐼 ) ) )
29 eqcom ⊢ ( 𝐼 = 𝑥 ↔ 𝑥 = 𝐼 )
30 29 orbi1i ⊢ ( ( 𝐼 = 𝑥 ∨ 𝑥 < 𝐼 ) ↔ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) )
31 30 notbii ⊢ ( ¬ ( 𝐼 = 𝑥 ∨ 𝑥 < 𝐼 ) ↔ ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) )
32 28 31 bitrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝐼 < 𝑥 ↔ ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) ) )
33 1zzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 1 ∈ ℤ )
34 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝑀 ∈ ℤ )
35 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝑥 ∈ ( 1 ... 𝑀 ) )
36 35 elfzelzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝑥 ∈ ℤ )
37 36 33 zsubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → ( 𝑥 − 1 ) ∈ ℤ )
38 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 1 ∈ ℝ )
39 22 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝐼 ∈ ℝ )
40 35 24 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝑥 ∈ ℝ )
41 2 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝐼 )
42 41 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 1 ≤ 𝐼 )
43 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 𝐼 < 𝑥 )
44 38 39 40 42 43 lelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 1 < 𝑥 )
45 33 36 zltlem1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → ( 1 < 𝑥 ↔ 1 ≤ ( 𝑥 − 1 ) ) )
46 44 45 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → 1 ≤ ( 𝑥 − 1 ) )
47 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 1 ∈ ℝ )
48 25 47 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝑥 − 1 ) ∈ ℝ )
49 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑀 ∈ ℝ )
50 0le1 ⊢ 0 ≤ 1
51 50 a1i ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 0 ≤ 1 )
52 1red ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
53 24 52 subge02d ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → ( 0 ≤ 1 ↔ ( 𝑥 − 1 ) ≤ 𝑥 ) )
54 51 53 mpbid ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → ( 𝑥 − 1 ) ≤ 𝑥 )
55 54 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝑥 − 1 ) ≤ 𝑥 )
56 elfzle2 ⊢ ( 𝑥 ∈ ( 1 ... 𝑀 ) → 𝑥 ≤ 𝑀 )
57 56 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → 𝑥 ≤ 𝑀 )
58 48 25 49 55 57 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝑥 − 1 ) ≤ 𝑀 )
59 58 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → ( 𝑥 − 1 ) ≤ 𝑀 )
60 33 34 37 46 59 elfzd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ∧ 𝐼 < 𝑥 ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) )
61 60 3expia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( 𝐼 < 𝑥 → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) ) )
62 32 61 sylbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → ( ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) ) )
63 62 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ ( 𝑥 = 𝐼 ∨ 𝑥 < 𝐼 ) ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) )
64 20 63 sylbi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ( ¬ 𝑥 = 𝐼 ∧ ¬ 𝑥 < 𝐼 ) ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) )
65 64 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝐼 ) ∧ ¬ 𝑥 < 𝐼 ) → ( 𝑥 − 1 ) ∈ ( 1 ... 𝑀 ) )
66 16 17 18 65 ifbothda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) ∧ ¬ 𝑥 = 𝐼 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ∈ ( 1 ... 𝑀 ) )
67 5 6 15 66 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ∈ ( 1 ... 𝑀 ) )
68 67 4 fmptd ⊢ ( 𝜑 → 𝐴 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )