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	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnfvalfi.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	sygbasnfpfi	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		psgnfvalfi.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnfvalfi.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1 2	symgbasf	⊢ ( 𝑃 ∈ 𝐵 → 𝑃 : 𝐷 ⟶ 𝐷 )
4	3	ffnd	⊢ ( 𝑃 ∈ 𝐵 → 𝑃 Fn 𝐷 )
5	4	adantl	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → 𝑃 Fn 𝐷 )
6		fndifnfp	⊢ ( 𝑃 Fn 𝐷 → dom ( 𝑃 ∖ I ) = { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } )
7	5 6	syl	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) = { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } )
8		rabfi	⊢ ( 𝐷 ∈ Fin → { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } ∈ Fin )
9	8	adantr	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝑃 ‘ 𝑥 ) ≠ 𝑥 } ∈ Fin )
10	7 9	eqeltrd	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵 ) → dom ( 𝑃 ∖ I ) ∈ Fin )