Theorem evpmval

Description: Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023)

	Ref	Expression
Hypothesis	evpmval.1	⊢ 𝐴 = ( pmEven ‘ 𝐷 )
Assertion	evpmval	⊢ ( 𝐷 ∈ 𝑉 → 𝐴 = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		evpmval.1	⊢ 𝐴 = ( pmEven ‘ 𝐷 )
2		elex	⊢ ( 𝐷 ∈ 𝑉 → 𝐷 ∈ V )
3		fveq2	⊢ ( 𝑑 = 𝐷 → ( pmSgn ‘ 𝑑 ) = ( pmSgn ‘ 𝐷 ) )
4	3	cnveqd	⊢ ( 𝑑 = 𝐷 → ◡ ( pmSgn ‘ 𝑑 ) = ◡ ( pmSgn ‘ 𝐷 ) )
5	4	imaeq1d	⊢ ( 𝑑 = 𝐷 → ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
6		df-evpm	⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )
7		fvex	⊢ ( pmSgn ‘ 𝐷 ) ∈ V
8	7	cnvex	⊢ ◡ ( pmSgn ‘ 𝐷 ) ∈ V
9	8	imaex	⊢ ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) ∈ V
10	5 6 9	fvmpt	⊢ ( 𝐷 ∈ V → ( pmEven ‘ 𝐷 ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
11	2 10	syl	⊢ ( 𝐷 ∈ 𝑉 → ( pmEven ‘ 𝐷 ) = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )
12	1 11	syl5eq	⊢ ( 𝐷 ∈ 𝑉 → 𝐴 = ( ◡ ( pmSgn ‘ 𝐷 ) “ { 1 } ) )