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