Theorem fzto1stfv1

Description: Value of our permutation P at 1. (Contributed by Thierry Arnoux, 23-Aug-2020)

	Ref	Expression
Hypotheses	psgnfzto1st.d	$$⊢D=\left(1\dots N\right)$$
	psgnfzto1st.p	$$⊢P=\left(i\in D⟼if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)\right)$$
Assertion	fzto1stfv1	$$⊢I\in D\to P\left(1\right)=I$$

Proof

Step	Hyp	Ref	Expression
1		psgnfzto1st.d	$$⊢D=\left(1\dots N\right)$$
2		psgnfzto1st.p	$$⊢P=\left(i\in D⟼if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)\right)$$
3		iftrue	$$⊢i=1\to if\left(i=1,I,if\left(i\le I,i-1,i\right)\right)=I$$
4		elfzuz2	$$⊢I\in \left(1\dots N\right)\to N\in {\mathbb{Z}}_{\ge 1}$$
5	4 1	eleq2s	$$⊢I\in D\to N\in {\mathbb{Z}}_{\ge 1}$$
6		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots N\right)$$
7	6 1	eleqtrrdi	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in D$$
8	5 7	syl	$$⊢I\in D\to 1\in D$$
9		id	$$⊢I\in D\to I\in D$$
10	2 3 8 9	fvmptd3	$$⊢I\in D\to P\left(1\right)=I$$