Theorem sygbasnfpfi

Description: The class of non-fixed points of a permutation of a finite set is finite. (Contributed by AV, 13-Jan-2019)

	Ref	Expression
Hypotheses	psgnfvalfi.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
	psgnfvalfi.b	$$⊢B={\mathrm{Base}}_G$$
Assertion	sygbasnfpfi	$$⊢\left(D\in \mathrm{Fin}\wedge P\in B\right)\to \mathrm{dom}\left(P\setminus \mathrm{I}\right)\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		psgnfvalfi.g	$$⊢G=\mathrm{SymGrp}\left(D\right)$$
2		psgnfvalfi.b	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbasf	$$⊢P\in B\to P:D⟶D$$
4	3	ffnd	$$⊢P\in B\to PFnD$$
5	4	adantl	$$⊢\left(D\in \mathrm{Fin}\wedge P\in B\right)\to PFnD$$
6		fndifnfp	$$⊢PFnD\to \mathrm{dom}\left(P\setminus \mathrm{I}\right)=\left\{x\in D|P\left(x\right)\ne x\right\}$$
7	5 6	syl	$$⊢\left(D\in \mathrm{Fin}\wedge P\in B\right)\to \mathrm{dom}\left(P\setminus \mathrm{I}\right)=\left\{x\in D|P\left(x\right)\ne x\right\}$$
8		rabfi	$$⊢D\in \mathrm{Fin}\to \left\{x\in D|P\left(x\right)\ne x\right\}\in \mathrm{Fin}$$
9	8	adantr	$$⊢\left(D\in \mathrm{Fin}\wedge P\in B\right)\to \left\{x\in D|P\left(x\right)\ne x\right\}\in \mathrm{Fin}$$
10	7 9	eqeltrd	$$⊢\left(D\in \mathrm{Fin}\wedge P\in B\right)\to \mathrm{dom}\left(P\setminus \mathrm{I}\right)\in \mathrm{Fin}$$