Theorem metakunt4

Description: Value of A. (Contributed by metakunt, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		metakunt4.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt4.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt4.3	$$⊢\phi \to I\le M$$
4		metakunt4.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=M,I,if\left(x<I,x,x+1\right)\right)\right)$$
5		metakunt4.5	$$⊢\phi \to X\in \left(1\dots M\right)$$
6	4	a1i	$$⊢\phi \to A=\left(x\in \left(1\dots M\right)⟼if\left(x=M,I,if\left(x<I,x,x+1\right)\right)\right)$$
7		eqeq1	$$⊢x=X\to \left(x=M\leftrightarrow X=M\right)$$
8		breq1	$$⊢x=X\to \left(x<I\leftrightarrow X<I\right)$$
9		id	$$⊢x=X\to x=X$$
10		oveq1	$$⊢x=X\to x+1=X+1$$
11	8 9 10	ifbieq12d	$$⊢x=X\to if\left(x<I,x,x+1\right)=if\left(X<I,X,X+1\right)$$
12	7 11	ifbieq2d	$$⊢x=X\to if\left(x=M,I,if\left(x<I,x,x+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
13	12	adantl	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=M,I,if\left(x<I,x,x+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
14	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
15	5	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
16	15	peano2zd	$$⊢\phi \to X+1\in \mathbb{Z}$$
17	15 16	ifcld	$$⊢\phi \to if\left(X<I,X,X+1\right)\in \mathbb{Z}$$
18	14 17	ifcld	$$⊢\phi \to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)\in \mathbb{Z}$$
19	6 13 5 18	fvmptd	$$⊢\phi \to A\left(X\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$