Theorem psgndmsubg

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

	Ref	Expression
Hypotheses	psgneldm.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgneldm.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
Assertion	psgndmsubg	$$⊢D\in V\to \mathrm{dom}N\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		psgneldm.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
2		psgneldm.n	$$⊢N=\mathrm{pmSgn}\left(D\right)$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4		eqid	$$⊢\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}=\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
5	1 3 4 2	psgnfn	$$⊢NFn\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
6		fndm	$$⊢NFn\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}\to \mathrm{dom}N=\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
7	5 6	ax-mp	$$⊢\mathrm{dom}N=\left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
8	1 3	symgfisg	$$⊢D\in V\to \left\{p\in {\mathrm{Base}}_G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}\in \mathrm{SubGrp}\left(G\right)$$
9	7 8	eqeltrid	$$⊢D\in V\to \mathrm{dom}N\in \mathrm{SubGrp}\left(G\right)$$