Theorem reprfz1

Description: Corollary of reprinfz1 . (Contributed by Thierry Arnoux, 14-Dec-2021)

	Ref	Expression
Hypotheses	reprfz1.n	|- ( ph -> N e. NN0 )
	reprfz1.s	|- ( ph -> S e. NN0 )
Assertion	reprfz1	|- ( ph -> ( NN ( repr ` S ) N ) = ( ( 1 ... N ) ( repr ` S ) N ) )

Proof

Step	Hyp	Ref	Expression
1		reprfz1.n	|- ( ph -> N e. NN0 )
2		reprfz1.s	|- ( ph -> S e. NN0 )
3		ssidd	|- ( ph -> NN C_ NN )
4	1 2 3	reprinfz1	|- ( ph -> ( NN ( repr ` S ) N ) = ( ( NN i^i ( 1 ... N ) ) ( repr ` S ) N ) )
5		fz1ssnn	|- ( 1 ... N ) C_ NN
6		dfss	|- ( ( 1 ... N ) C_ NN <-> ( 1 ... N ) = ( ( 1 ... N ) i^i NN ) )
7	5 6	mpbi	|- ( 1 ... N ) = ( ( 1 ... N ) i^i NN )
8		incom	|- ( ( 1 ... N ) i^i NN ) = ( NN i^i ( 1 ... N ) )
9	7 8	eqtri	|- ( 1 ... N ) = ( NN i^i ( 1 ... N ) )
10	9	oveq1i	|- ( ( 1 ... N ) ( repr ` S ) N ) = ( ( NN i^i ( 1 ... N ) ) ( repr ` S ) N )
11	4 10	eqtr4di	|- ( ph -> ( NN ( repr ` S ) N ) = ( ( 1 ... N ) ( repr ` S ) N ) )