Theorem psgneldm

Description: Property of being a finitary permutation. (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)$$
	psgneldm.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	psgneldm	$$⊢P\in \mathrm{dom}N\leftrightarrow \left(P\in B\wedge \mathrm{dom}\left(P\setminus \mathrm{I}\right)\in \mathrm{Fin}\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		psgneldm.b	$$⊢B={\mathrm{Base}}_G$$
4		difeq1	$$⊢p=P\to p\setminus \mathrm{I}=P\setminus \mathrm{I}$$
5	4	dmeqd	$$⊢p=P\to \mathrm{dom}\left(p\setminus \mathrm{I}\right)=\mathrm{dom}\left(P\setminus \mathrm{I}\right)$$
6	5	eleq1d	$$⊢p=P\to \left(\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\leftrightarrow \mathrm{dom}\left(P\setminus \mathrm{I}\right)\in \mathrm{Fin}\right)$$
7		eqid	$$⊢\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}=\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
8	1 3 7 2	psgnfn	$$⊢NFn\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
9	8	fndmi	$$⊢\mathrm{dom}N=\left\{p\in B|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
10	6 9	elrab2	$$⊢P\in \mathrm{dom}N\leftrightarrow \left(P\in B\wedge \mathrm{dom}\left(P\setminus \mathrm{I}\right)\in \mathrm{Fin}\right)$$