This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )