Theorem fzto1stfv1

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

	Ref	Expression
Hypotheses	psgnfzto1st.d	|- D = ( 1 ... N )
	psgnfzto1st.p	|- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
Assertion	fzto1stfv1	|- ( I e. D -> ( P ` 1 ) = I )

Proof

Step	Hyp	Ref	Expression
1		psgnfzto1st.d	|- D = ( 1 ... N )
2		psgnfzto1st.p	|- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )
3		iftrue	|- ( i = 1 -> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) = I )
4		elfzuz2	|- ( I e. ( 1 ... N ) -> N e. ( ZZ>= ` 1 ) )
5	4 1	eleq2s	|- ( I e. D -> N e. ( ZZ>= ` 1 ) )
6		eluzfz1	|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
7	6 1	eleqtrrdi	|- ( N e. ( ZZ>= ` 1 ) -> 1 e. D )
8	5 7	syl	|- ( I e. D -> 1 e. D )
9		id	|- ( I e. D -> I e. D )
10	2 3 8 9	fvmptd3	|- ( I e. D -> ( P ` 1 ) = I )