Theorem metakunt9

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

	Ref	Expression
Hypotheses	metakunt9.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt9.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt9.3	$$⊢\phi \to I\le M$$
	metakunt9.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)$$
	metakunt9.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)$$
	metakunt9.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
Assertion	metakunt9	$$⊢\phi \to C\left(A\left(X\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		metakunt9.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt9.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt9.3	$$⊢\phi \to I\le M$$
4		metakunt9.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		metakunt9.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		metakunt9.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7	1 2 3 4 5 6	metakunt8	$$⊢\left(\phi \wedge I<X\right)\to C\left(A\left(X\right)\right)=X$$
8		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
9	6 8	syl	$$⊢\phi \to X\in \mathbb{N}$$
10	9	nnred	$$⊢\phi \to X\in ℝ$$
11	2	nnred	$$⊢\phi \to I\in ℝ$$
12	10 11	leloed	$$⊢\phi \to \left(X\le I\leftrightarrow \left(X<I\vee X=I\right)\right)$$
13	1 2 3 4 5 6	metakunt6	$$⊢\left(\phi \wedge X<I\right)\to C\left(A\left(X\right)\right)=X$$
14	1 2 3 4 5 6	metakunt5	$$⊢\left(\phi \wedge X=I\right)\to C\left(A\left(X\right)\right)=X$$
15	13 14	jaodan	$$⊢\left(\phi \wedge \left(X<I\vee X=I\right)\right)\to C\left(A\left(X\right)\right)=X$$
16	15	ex	$$⊢\phi \to \left(\left(X<I\vee X=I\right)\to C\left(A\left(X\right)\right)=X\right)$$
17	12 16	sylbid	$$⊢\phi \to \left(X\le I\to C\left(A\left(X\right)\right)=X\right)$$
18	17	imp	$$⊢\left(\phi \wedge X\le I\right)\to C\left(A\left(X\right)\right)=X$$
19	7 18 11 10	ltlecasei	$$⊢\phi \to C\left(A\left(X\right)\right)=X$$