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 = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cevpm | ⊢ pmEven | |
1 | vd | ⊢ 𝑑 | |
2 | cvv | ⊢ V | |
3 | cpsgn | ⊢ pmSgn | |
4 | 1 | cv | ⊢ 𝑑 |
5 | 4 3 | cfv | ⊢ ( pmSgn ‘ 𝑑 ) |
6 | 5 | ccnv | ⊢ ◡ ( pmSgn ‘ 𝑑 ) |
7 | c1 | ⊢ 1 | |
8 | 7 | csn | ⊢ { 1 } |
9 | 6 8 | cima | ⊢ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) |
10 | 1 2 9 | cmpt | ⊢ ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) ) |
11 | 0 10 | wceq | ⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) ) |