Theorem psgnfn

Description: Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015)

	Ref	Expression
Hypotheses	psgnfn.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
	psgnfn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	psgnfn.f	⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
	psgnfn.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
Assertion	psgnfn	⊢ 𝑁 Fn 𝐹

Proof

Step	Hyp	Ref	Expression
1		psgnfn.g	⊢ 𝐺 = ( SymGrp ‘ 𝐷 )
2		psgnfn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		psgnfn.f	⊢ 𝐹 = { 𝑝 ∈ 𝐵 ∣ dom ( 𝑝 ∖ I ) ∈ Fin }
4		psgnfn.n	⊢ 𝑁 = ( pmSgn ‘ 𝐷 )
5		iotaex	⊢ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) ∈ V
6		eqid	⊢ ran ( pmTrsp ‘ 𝐷 ) = ran ( pmTrsp ‘ 𝐷 )
7	1 2 3 6 4	psgnfval	⊢ 𝑁 = ( 𝑥 ∈ 𝐹 ↦ ( ℩ 𝑠 ∃ 𝑤 ∈ Word ran ( pmTrsp ‘ 𝐷 ) ( 𝑥 = ( 𝐺 Σg 𝑤 ) ∧ 𝑠 = ( - 1 ↑ ( ♯ ‘ 𝑤 ) ) ) ) )
8	5 7	fnmpti	⊢ 𝑁 Fn 𝐹