This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-evpm

Description: Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018)

		Ref	Expression
	Assertion	df-evpm	$⊢ pmEven = (d \in V ⟼ {pmSgn (d)}^{-1} [\{1\}])$

Step	Hyp	Ref	Expression
0		cevpm	$class pmEven$
1		vd	$setvar d$
2		cvv	$class V$
3		cpsgn	$class pmSgn$
4	1	cv	$setvar d$
5	4 3	cfv	$class pmSgn (d)$
6	5	ccnv	$class {pmSgn (d)}^{-1}$
7		c1	$class 1$
8	7	csn	$class \{1\}$
9	6 8	cima	$class {pmSgn (d)}^{-1} [\{1\}]$
10	1 2 9	cmpt	$class (d \in V ⟼ {pmSgn (d)}^{-1} [\{1\}])$
11	0 10	wceq	$wff pmEven = (d \in V ⟼ {pmSgn (d)}^{-1} [\{1\}])$