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