Theorem metakunt34

Description: D is a permutation. (Contributed by metakunt, 18-Jul-2024)

	Ref	Expression
Hypotheses	metakunt34.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt34.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt34.3	$$⊢\phi \to I\le M$$
	metakunt34.4	$$⊢D=\left(w\in \left(1\dots M\right)⟼if\left(w=I,w,if\left(w<I,w+\left(M-I\right)+if\left(I\le w+M-I,1,0\right),w-I+if\left(I\le w-I,1,0\right)\right)\right)\right)$$
Assertion	metakunt34	$$⊢\phi \to D:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$

Proof

Step	Hyp	Ref	Expression
1		metakunt34.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt34.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt34.3	$$⊢\phi \to I\le M$$
4		metakunt34.4	$$⊢D=\left(w\in \left(1\dots M\right)⟼if\left(w=I,w,if\left(w<I,w+\left(M-I\right)+if\left(I\le w+M-I,1,0\right),w-I+if\left(I\le w-I,1,0\right)\right)\right)\right)$$
5		eqid	$$⊢\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
6		eqid	$$⊢\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)=\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)$$
7	1 2 3 5 6	metakunt14	$$⊢\phi \to \left(\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\wedge {\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)}^{-1}=\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)\right)$$
8	7	simpld	$$⊢\phi \to \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
9		f1ocnv	$$⊢\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\to {\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)}^{-1}:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
10	8 9	syl	$$⊢\phi \to {\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)}^{-1}:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
11	7	simprd	$$⊢\phi \to {\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)}^{-1}=\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)$$
12	11	f1oeq1d	$$⊢\phi \to \left({\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)}^{-1}:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\leftrightarrow \left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\right)$$
13	10 12	mpbid	$$⊢\phi \to \left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
14		eqid	$$⊢\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)=\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)$$
15	1 2 3 14	metakunt25	$$⊢\phi \to \left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
16		f1oco	$$⊢\left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\wedge \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\right)\to \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
17	15 8 16	syl2anc	$$⊢\phi \to \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
18		f1oco	$$⊢\left(\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\wedge \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\right)\to \left(\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)\circ \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
19	13 17 18	syl2anc	$$⊢\phi \to \left(\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)\circ \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$
20	1 2 3 5 14 6 4	metakunt33	$$⊢\phi \to \left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)\circ \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right)=D$$
21	20	f1oeq1d	$$⊢\phi \to \left(\left(\left(z\in \left(1\dots M\right)⟼if\left(z=M,I,if\left(z<I,z,z+1\right)\right)\right)\circ \left(\left(y\in \left(1\dots M\right)⟼if\left(y=M,M,if\left(y<I,y+M-I,y+1-I\right)\right)\right)\circ \left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)\right)\right):\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\leftrightarrow D:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)\right)$$
22	19 21	mpbid	$$⊢\phi \to D:\left(1\dots M\right)\underset{1-1\; onto}{⟶}\left(1\dots M\right)$$