Theorem psgndmfi

Description: For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020)

	Ref	Expression
Hypotheses	psgndmfi.s	⊢ 𝑆 = ( pmSgn ‘ 𝐷 )
	psgndmfi.g	⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
Assertion	psgndmfi	⊢ ( 𝐷 ∈ Fin → 𝑆 Fn 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		psgndmfi.s	⊢ 𝑆 = ( pmSgn ‘ 𝐷 )
2		psgndmfi.g	⊢ 𝐺 = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
3		eqid	⊢ ( SymGrp ‘ 𝐷 ) = ( SymGrp ‘ 𝐷 )
4		eqid	⊢ { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
5	3 2 4 1	psgnfn	⊢ 𝑆 Fn { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
6	3 2	sygbasnfpfi	⊢ ( ( 𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐺 ) → dom ( 𝑝 ∖ I ) ∈ Fin )
7	6	ralrimiva	⊢ ( 𝐷 ∈ Fin → ∀ 𝑝 ∈ 𝐺 dom ( 𝑝 ∖ I ) ∈ Fin )
8		rabid2	⊢ ( 𝐺 = { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↔ ∀ 𝑝 ∈ 𝐺 dom ( 𝑝 ∖ I ) ∈ Fin )
9	7 8	sylibr	⊢ ( 𝐷 ∈ Fin → 𝐺 = { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } )
10	9	eqcomd	⊢ ( 𝐷 ∈ Fin → { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } = 𝐺 )
11	10	fneq2d	⊢ ( 𝐷 ∈ Fin → ( 𝑆 Fn { 𝑝 ∈ 𝐺 ∣ dom ( 𝑝 ∖ I ) ∈ Fin } ↔ 𝑆 Fn 𝐺 ) )
12	5 11	mpbii	⊢ ( 𝐷 ∈ Fin → 𝑆 Fn 𝐺 )