Theorem reprfi2

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

	Ref	Expression
Hypotheses	reprinfz1.n	|- ( ph -> N e. NN0 )
	reprinfz1.s	|- ( ph -> S e. NN0 )
	reprinfz1.a	|- ( ph -> A C_ NN )
Assertion	reprfi2	|- ( ph -> ( A ( repr ` S ) N ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		reprinfz1.n	|- ( ph -> N e. NN0 )
2		reprinfz1.s	|- ( ph -> S e. NN0 )
3		reprinfz1.a	|- ( ph -> A C_ NN )
4	1 2 3	reprinfz1	|- ( ph -> ( A ( repr ` S ) N ) = ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) )
5		inss2	|- ( A i^i ( 1 ... N ) ) C_ ( 1 ... N )
6		fz1ssnn	|- ( 1 ... N ) C_ NN
7	5 6	sstri	|- ( A i^i ( 1 ... N ) ) C_ NN
8	7	a1i	|- ( ph -> ( A i^i ( 1 ... N ) ) C_ NN )
9	1	nn0zd	|- ( ph -> N e. ZZ )
10		fzfi	|- ( 1 ... N ) e. Fin
11	10	a1i	|- ( ph -> ( 1 ... N ) e. Fin )
12	5	a1i	|- ( ph -> ( A i^i ( 1 ... N ) ) C_ ( 1 ... N ) )
13	11 12	ssfid	|- ( ph -> ( A i^i ( 1 ... N ) ) e. Fin )
14	8 9 2 13	reprfi	|- ( ph -> ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) e. Fin )
15	4 14	eqeltrd	|- ( ph -> ( A ( repr ` S ) N ) e. Fin )