| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mplvrpmlem.s |
|- S = ( SymGrp ` I ) |
| 2 |
|
mplvrpmlem.p |
|- P = ( Base ` S ) |
| 3 |
|
mplvrpmlem.i |
|- ( ph -> I e. V ) |
| 4 |
|
mplvrpmlem.d |
|- ( ph -> D e. P ) |
| 5 |
|
mplvrpmlem.1 |
|- ( ph -> X e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) |
| 6 |
|
breq1 |
|- ( h = ( X o. D ) -> ( h finSupp 0 <-> ( X o. D ) finSupp 0 ) ) |
| 7 |
|
nn0ex |
|- NN0 e. _V |
| 8 |
7
|
a1i |
|- ( ph -> NN0 e. _V ) |
| 9 |
|
ssrab2 |
|- { h e. ( NN0 ^m I ) | h finSupp 0 } C_ ( NN0 ^m I ) |
| 10 |
9 5
|
sselid |
|- ( ph -> X e. ( NN0 ^m I ) ) |
| 11 |
3 8 10
|
elmaprd |
|- ( ph -> X : I --> NN0 ) |
| 12 |
1 2
|
symgbasf1o |
|- ( D e. P -> D : I -1-1-onto-> I ) |
| 13 |
4 12
|
syl |
|- ( ph -> D : I -1-1-onto-> I ) |
| 14 |
|
f1of |
|- ( D : I -1-1-onto-> I -> D : I --> I ) |
| 15 |
13 14
|
syl |
|- ( ph -> D : I --> I ) |
| 16 |
11 15
|
fcod |
|- ( ph -> ( X o. D ) : I --> NN0 ) |
| 17 |
8 3 16
|
elmapdd |
|- ( ph -> ( X o. D ) e. ( NN0 ^m I ) ) |
| 18 |
|
breq1 |
|- ( h = X -> ( h finSupp 0 <-> X finSupp 0 ) ) |
| 19 |
18
|
elrab |
|- ( X e. { h e. ( NN0 ^m I ) | h finSupp 0 } <-> ( X e. ( NN0 ^m I ) /\ X finSupp 0 ) ) |
| 20 |
19
|
simprbi |
|- ( X e. { h e. ( NN0 ^m I ) | h finSupp 0 } -> X finSupp 0 ) |
| 21 |
5 20
|
syl |
|- ( ph -> X finSupp 0 ) |
| 22 |
|
f1of1 |
|- ( D : I -1-1-onto-> I -> D : I -1-1-> I ) |
| 23 |
13 22
|
syl |
|- ( ph -> D : I -1-1-> I ) |
| 24 |
|
0nn0 |
|- 0 e. NN0 |
| 25 |
24
|
a1i |
|- ( ph -> 0 e. NN0 ) |
| 26 |
21 23 25 5
|
fsuppco |
|- ( ph -> ( X o. D ) finSupp 0 ) |
| 27 |
6 17 26
|
elrabd |
|- ( ph -> ( X o. D ) e. { h e. ( NN0 ^m I ) | h finSupp 0 } ) |