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