| Step |
Hyp |
Ref |
Expression |
| 1 |
|
psgneldm.g |
|- G = ( SymGrp ` D ) |
| 2 |
|
psgneldm.n |
|- N = ( pmSgn ` D ) |
| 3 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
| 4 |
|
eqid |
|- { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 5 |
1 3 4 2
|
psgnfn |
|- N Fn { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 6 |
|
fndm |
|- ( N Fn { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } -> dom N = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } ) |
| 7 |
5 6
|
ax-mp |
|- dom N = { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } |
| 8 |
1 3
|
symgfisg |
|- ( D e. V -> { p e. ( Base ` G ) | dom ( p \ _I ) e. Fin } e. ( SubGrp ` G ) ) |
| 9 |
7 8
|
eqeltrid |
|- ( D e. V -> dom N e. ( SubGrp ` G ) ) |