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 = ( SymGrp ` D )
	psgnfvalfi.b	|- B = ( Base ` G )
Assertion	sygbasnfpfi	|- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		psgnfvalfi.g	|- G = ( SymGrp ` D )
2		psgnfvalfi.b	|- B = ( Base ` G )
3	1 2	symgbasf	|- ( P e. B -> P : D --> D )
4	3	ffnd	|- ( P e. B -> P Fn D )
5	4	adantl	|- ( ( D e. Fin /\ P e. B ) -> P Fn D )
6		fndifnfp	|- ( P Fn D -> dom ( P \ _I ) = { x e. D | ( P ` x ) =/= x } )
7	5 6	syl	|- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) = { x e. D | ( P ` x ) =/= x } )
8		rabfi	|- ( D e. Fin -> { x e. D | ( P ` x ) =/= x } e. Fin )
9	8	adantr	|- ( ( D e. Fin /\ P e. B ) -> { x e. D | ( P ` x ) =/= x } e. Fin )
10	7 9	eqeltrd	|- ( ( D e. Fin /\ P e. B ) -> dom ( P \ _I ) e. Fin )