Theorem psgndmfi

Description: For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020)

	Ref	Expression
Hypotheses	psgndmfi.s	|- S = ( pmSgn ` D )
	psgndmfi.g	|- G = ( Base ` ( SymGrp ` D ) )
Assertion	psgndmfi	|- ( D e. Fin -> S Fn G )

Proof

Step	Hyp	Ref	Expression
1		psgndmfi.s	|- S = ( pmSgn ` D )
2		psgndmfi.g	|- G = ( Base ` ( SymGrp ` D ) )
3		eqid	|- ( SymGrp ` D ) = ( SymGrp ` D )
4		eqid	|- { p e. G | dom ( p \ _I ) e. Fin } = { p e. G | dom ( p \ _I ) e. Fin }
5	3 2 4 1	psgnfn	|- S Fn { p e. G | dom ( p \ _I ) e. Fin }
6	3 2	sygbasnfpfi	|- ( ( D e. Fin /\ p e. G ) -> dom ( p \ _I ) e. Fin )
7	6	ralrimiva	|- ( D e. Fin -> A. p e. G dom ( p \ _I ) e. Fin )
8		rabid2	|- ( G = { p e. G | dom ( p \ _I ) e. Fin } <-> A. p e. G dom ( p \ _I ) e. Fin )
9	7 8	sylibr	|- ( D e. Fin -> G = { p e. G | dom ( p \ _I ) e. Fin } )
10	9	eqcomd	|- ( D e. Fin -> { p e. G | dom ( p \ _I ) e. Fin } = G )
11	10	fneq2d	|- ( D e. Fin -> ( S Fn { p e. G | dom ( p \ _I ) e. Fin } <-> S Fn G ) )
12	5 11	mpbii	|- ( D e. Fin -> S Fn G )