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	|- A = ( pmEven ` D )
Assertion	evpmval	|- ( D e. V -> A = ( `' ( pmSgn ` D ) " { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		evpmval.1	|- A = ( pmEven ` D )
2		elex	|- ( D e. V -> D e. _V )
3		fveq2	|- ( d = D -> ( pmSgn ` d ) = ( pmSgn ` D ) )
4	3	cnveqd	|- ( d = D -> `' ( pmSgn ` d ) = `' ( pmSgn ` D ) )
5	4	imaeq1d	|- ( d = D -> ( `' ( pmSgn ` d ) " { 1 } ) = ( `' ( pmSgn ` D ) " { 1 } ) )
6		df-evpm	|- pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )
7		fvex	|- ( pmSgn ` D ) e. _V
8	7	cnvex	|- `' ( pmSgn ` D ) e. _V
9	8	imaex	|- ( `' ( pmSgn ` D ) " { 1 } ) e. _V
10	5 6 9	fvmpt	|- ( D e. _V -> ( pmEven ` D ) = ( `' ( pmSgn ` D ) " { 1 } ) )
11	2 10	syl	|- ( D e. V -> ( pmEven ` D ) = ( `' ( pmSgn ` D ) " { 1 } ) )
12	1 11	syl5eq	|- ( D e. V -> A = ( `' ( pmSgn ` D ) " { 1 } ) )