Metamath Proof Explorer

Theorem metakunt11

Description: C is the right inverse for A. (Contributed by metakunt, 24-May-2024)

Ref Expression
Hypotheses metakunt11.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt11.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt11.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt11.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt11.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
metakunt11.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
Assertion metakunt11 ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 metakunt11.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt11.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt11.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt11.4 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5 metakunt11.5 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6 metakunt11.6 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7 4 a1i ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
8 eqeq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 = 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) = 𝐼 ) )
9 breq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 < 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) < 𝐼 ) )
10 id ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → 𝑥 = ( 𝐶 ‘ 𝑋 ) )
11 oveq1 ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → ( 𝑥 − 1 ) = ( ( 𝐶 ‘ 𝑋 ) − 1 ) )
12 9 10 11 ifbieq12d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
13 8 12 ifbieq2d ⊢ ( 𝑥 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
15 5 a1i ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
16 eqeq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 = 𝑀 ↔ 𝑋 = 𝑀 ) )
17 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 < 𝐼 ↔ 𝑋 < 𝐼 ) )
18 id ⊢ ( 𝑦 = 𝑋 → 𝑦 = 𝑋 )
19 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 1 ) = ( 𝑋 + 1 ) )
20 17 18 19 ifbieq12d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
21 16 20 ifbieq2d ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
22 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )
23 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
24 6 23 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
25 24 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ℝ )
27 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐼 ∈ ℝ )
29 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑀 ∈ ℝ )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝐼 )
32 3 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐼 ≤ 𝑀 )
33 26 28 30 31 32 ltletrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 < 𝑀 )
34 26 33 ltned ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ≠ 𝑀 )
35 df-ne ⊢ ( 𝑋 ≠ 𝑀 ↔ ¬ 𝑋 = 𝑀 )
36 34 35 sylib ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝑀 )
37 iffalse ⊢ ( ¬ 𝑋 = 𝑀 → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) )
39 iftrue ⊢ ( 𝑋 < 𝐼 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = 𝑋 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) = 𝑋 )
41 38 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = 𝑋 )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) = 𝑋 )
43 22 42 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑦 = 𝑋 ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = 𝑋 )
44 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ∈ ( 1 ... 𝑀 ) )
45 15 43 44 44 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ 𝑋 ) = 𝑋 )
46 eqeq1 ⊢ ( ( 𝐶 ‘ 𝑋 ) = 𝑋 → ( ( 𝐶 ‘ 𝑋 ) = 𝐼 ↔ 𝑋 = 𝐼 ) )
47 46 ifbid ⊢ ( ( 𝐶 ‘ 𝑋 ) = 𝑋 → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
48 45 47 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) )
49 26 31 ltned ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 ≠ 𝐼 )
50 49 neneqd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ¬ 𝑋 = 𝐼 )
51 iffalse ⊢ ( ¬ 𝑋 = 𝐼 → if ( 𝑋 = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
53 45 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝑋 = ( 𝐶 ‘ 𝑋 ) )
54 breq1 ⊢ ( 𝑋 = ( 𝐶 ‘ 𝑋 ) → ( 𝑋 < 𝐼 ↔ ( 𝐶 ‘ 𝑋 ) < 𝐼 ) )
55 id ⊢ ( 𝑋 = ( 𝐶 ‘ 𝑋 ) → 𝑋 = ( 𝐶 ‘ 𝑋 ) )
56 oveq1 ⊢ ( 𝑋 = ( 𝐶 ‘ 𝑋 ) → ( 𝑋 − 1 ) = ( ( 𝐶 ‘ 𝑋 ) − 1 ) )
57 54 55 56 ifbieq12d ⊢ ( 𝑋 = ( 𝐶 ‘ 𝑋 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
58 53 57 syl ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) )
59 58 eqcomd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
60 31 iftrued ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) = 𝑋 )
61 59 60 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) = 𝑋 )
62 52 61 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( 𝑋 = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
63 48 62 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
64 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( ( 𝐶 ‘ 𝑋 ) = 𝐼 , 𝑀 , if ( ( 𝐶 ‘ 𝑋 ) < 𝐼 , ( 𝐶 ‘ 𝑋 ) , ( ( 𝐶 ‘ 𝑋 ) − 1 ) ) ) = 𝑋 )
65 14 64 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 < 𝐼 ) ∧ 𝑥 = ( 𝐶 ‘ 𝑋 ) ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = 𝑋 )
66 1 2 3 5 metakunt2 ⊢ ( 𝜑 → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → 𝐶 : ( 1 ... 𝑀 ) ⟶ ( 1 ... 𝑀 ) )
68 67 44 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐶 ‘ 𝑋 ) ∈ ( 1 ... 𝑀 ) )
69 7 65 68 44 fvmptd ⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )