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 e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cevpm | |- pmEven |
|
1 | vd | |- d |
|
2 | cvv | |- _V |
|
3 | cpsgn | |- pmSgn |
|
4 | 1 | cv | |- d |
5 | 4 3 | cfv | |- ( pmSgn ` d ) |
6 | 5 | ccnv | |- `' ( pmSgn ` d ) |
7 | c1 | |- 1 |
|
8 | 7 | csn | |- { 1 } |
9 | 6 8 | cima | |- ( `' ( pmSgn ` d ) " { 1 } ) |
10 | 1 2 9 | cmpt | |- ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) ) |
11 | 0 10 | wceq | |- pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) ) |