Theorem metakunt13

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

	Ref	Expression
Hypotheses	metakunt13.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt13.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt13.3	$$⊢\phi \to I\le M$$
	metakunt13.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
	metakunt13.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
	metakunt13.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
Assertion	metakunt13	$$⊢\phi \to A\left(C\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		metakunt13.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt13.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt13.3	$$⊢\phi \to I\le M$$
4		metakunt13.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
5		metakunt13.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
6		metakunt13.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7	1 2 3 4 5 6	metakunt10	$$⊢\left(\phi \wedge X=M\right)\to A\left(C\left(X\right)\right)=X$$
8	7	ex	$$⊢\phi \to \left(X=M\to A\left(C\left(X\right)\right)=X\right)$$
9	1 2 3 4 5 6	metakunt11	$$⊢\left(\phi \wedge X<I\right)\to A\left(C\left(X\right)\right)=X$$
10	9	ex	$$⊢\phi \to \left(X<I\to A\left(C\left(X\right)\right)=X\right)$$
11	1 2 3 4 5 6	metakunt12	$$⊢\left(\phi \wedge \neg \left(X=M\vee X<I\right)\right)\to A\left(C\left(X\right)\right)=X$$
12	11	ex	$$⊢\phi \to \left(\neg \left(X=M\vee X<I\right)\to A\left(C\left(X\right)\right)=X\right)$$
13	8 10 12	ecase3d	$$⊢\phi \to A\left(C\left(X\right)\right)=X$$