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