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 ⊢ G = SymGrp ⁡ D
psgnfvalfi.b ⊢ B = Base G
Assertion sygbasnfpfi ⊢ D ∈ Fin ∧ P ∈ B → dom ⁡ P ∖ I ∈ Fin

Proof

Step Hyp Ref Expression
1 psgnfvalfi.g ⊢ G = SymGrp ⁡ D
2 psgnfvalfi.b ⊢ B = Base G
3 1 2 symgbasf ⊢ P ∈ B → P : D ⟶ D
4 3 ffnd ⊢ P ∈ B → P Fn D
5 4 adantl ⊢ D ∈ Fin ∧ P ∈ B → P Fn D
6 fndifnfp ⊢ P Fn D → dom ⁡ P ∖ I = x ∈ D | P ⁡ x ≠ x
7 5 6 syl ⊢ D ∈ Fin ∧ P ∈ B → dom ⁡ P ∖ I = x ∈ D | P ⁡ x ≠ x
8 rabfi ⊢ D ∈ Fin → x ∈ D | P ⁡ x ≠ x ∈ Fin
9 8 adantr ⊢ D ∈ Fin ∧ P ∈ B → x ∈ D | P ⁡ x ≠ x ∈ Fin
10 7 9 eqeltrd ⊢ D ∈ Fin ∧ P ∈ B → dom ⁡ P ∖ I ∈ Fin