| 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 ) ) |