Metamath Proof Explorer


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 )