Theorem psgneldm

Description: Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	psgneldm.g	|- G = ( SymGrp ` D )
	psgneldm.n	|- N = ( pmSgn ` D )
	psgneldm.b	|- B = ( Base ` G )
Assertion	psgneldm	|- ( P e. dom N <-> ( P e. B /\ dom ( P \ _I ) e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		psgneldm.g	|- G = ( SymGrp ` D )
2		psgneldm.n	|- N = ( pmSgn ` D )
3		psgneldm.b	|- B = ( Base ` G )
4		difeq1	|- ( p = P -> ( p \ _I ) = ( P \ _I ) )
5	4	dmeqd	|- ( p = P -> dom ( p \ _I ) = dom ( P \ _I ) )
6	5	eleq1d	|- ( p = P -> ( dom ( p \ _I ) e. Fin <-> dom ( P \ _I ) e. Fin ) )
7		eqid	|- { p e. B | dom ( p \ _I ) e. Fin } = { p e. B | dom ( p \ _I ) e. Fin }
8	1 3 7 2	psgnfn	|- N Fn { p e. B | dom ( p \ _I ) e. Fin }
9	8	fndmi	|- dom N = { p e. B | dom ( p \ _I ) e. Fin }
10	6 9	elrab2	|- ( P e. dom N <-> ( P e. B /\ dom ( P \ _I ) e. Fin ) )