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=\mathrm{pmSgn}\left(D\right)$$
	psgndmfi.g	$$⊢G={\mathrm{Base}}_{\mathrm{SymGrp}\left(D\right)}$$
Assertion	psgndmfi	$$⊢D\in \mathrm{Fin}\to SFnG$$

Proof

Step	Hyp	Ref	Expression
1		psgndmfi.s	$$⊢S=\mathrm{pmSgn}\left(D\right)$$
2		psgndmfi.g	$$⊢G={\mathrm{Base}}_{\mathrm{SymGrp}\left(D\right)}$$
3		eqid	$$⊢\mathrm{SymGrp}\left(D\right)=\mathrm{SymGrp}\left(D\right)$$
4		eqid	$$⊢\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}=\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
5	3 2 4 1	psgnfn	$$⊢SFn\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
6	3 2	sygbasnfpfi	$$⊢\left(D\in \mathrm{Fin}\wedge p\in G\right)\to \mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
7	6	ralrimiva	$$⊢D\in \mathrm{Fin}\to \forall p\in G\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
8		rabid2	$$⊢G=\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}\leftrightarrow \forall p\in G\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}$$
9	7 8	sylibr	$$⊢D\in \mathrm{Fin}\to G=\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}$$
10	9	eqcomd	$$⊢D\in \mathrm{Fin}\to \left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}=G$$
11	10	fneq2d	$$⊢D\in \mathrm{Fin}\to \left(SFn\left\{p\in G|\mathrm{dom}\left(p\setminus \mathrm{I}\right)\in \mathrm{Fin}\right\}\leftrightarrow SFnG\right)$$
12	5 11	mpbii	$$⊢D\in \mathrm{Fin}\to SFnG$$