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 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 )