Metamath Proof Explorer


Theorem psgndmsubg

Description: The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypotheses psgneldm.g
|- G = ( SymGrp ` D )
psgneldm.n
|- N = ( pmSgn ` D )
Assertion psgndmsubg
|- ( D e. V -> dom N e. ( SubGrp ` G ) )

Proof

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