Theorem metakunt13

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt13.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt13.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt13.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4		metakunt13.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5		metakunt13.5	⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
6		metakunt13.6	⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
7	1 2 3 4 5 6	metakunt10	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑀 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )
8	7	ex	⊢ ( 𝜑 → ( 𝑋 = 𝑀 → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 ) )
9	1 2 3 4 5 6	metakunt11	⊢ ( ( 𝜑 ∧ 𝑋 < 𝐼 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )
10	9	ex	⊢ ( 𝜑 → ( 𝑋 < 𝐼 → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 ) )
11	1 2 3 4 5 6	metakunt12	⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 = 𝑀 ∨ 𝑋 < 𝐼 ) ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )
12	11	ex	⊢ ( 𝜑 → ( ¬ ( 𝑋 = 𝑀 ∨ 𝑋 < 𝐼 ) → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 ) )
13	8 10 12	ecase3d	⊢ ( 𝜑 → ( 𝐴 ‘ ( 𝐶 ‘ 𝑋 ) ) = 𝑋 )