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=\mathrm{pmEven}\left(D\right)$$
Assertion	evpmval	$$⊢D\in V\to A={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		evpmval.1	$$⊢A=\mathrm{pmEven}\left(D\right)$$
2		elex	$$⊢D\in V\to D\in \mathrm{V}$$
3		fveq2	$$⊢d=D\to \mathrm{pmSgn}\left(d\right)=\mathrm{pmSgn}\left(D\right)$$
4	3	cnveqd	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}={\mathrm{pmSgn}\left(D\right)}^{-1}$$
5	4	imaeq1d	$$⊢d=D\to {\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
6		df-evpm	$$⊢\mathrm{pmEven}=\left(d\in \mathrm{V}⟼{\mathrm{pmSgn}\left(d\right)}^{-1}\left[\left\{1\right\}\right]\right)$$
7		fvex	$$⊢\mathrm{pmSgn}\left(D\right)\in \mathrm{V}$$
8	7	cnvex	$$⊢{\mathrm{pmSgn}\left(D\right)}^{-1}\in \mathrm{V}$$
9	8	imaex	$$⊢{\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{V}$$
10	5 6 9	fvmpt	$$⊢D\in \mathrm{V}\to \mathrm{pmEven}\left(D\right)={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
11	2 10	syl	$$⊢D\in V\to \mathrm{pmEven}\left(D\right)={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$
12	1 11	syl5eq	$$⊢D\in V\to A={\mathrm{pmSgn}\left(D\right)}^{-1}\left[\left\{1\right\}\right]$$