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

Metamath Proof Explorer

Definition df-pmtr

Description: Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion df-pmtr ⊢ pmTrsp = d ∈ V ⟼ p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpmtr class pmTrsp
1 vd setvar d
2 cvv class V
3 vp setvar p
4 vy setvar y
5 1 cv setvar d
6 5 cpw class 𝒫 d
7 4 cv setvar y
8 cen class ≈
9 c2o class 2 𝑜
10 7 9 8 wbr wff y ≈ 2 𝑜
11 10 4 6 crab class y ∈ 𝒫 d | y ≈ 2 𝑜
12 vz setvar z
13 12 cv setvar z
14 3 cv setvar p
15 13 14 wcel wff z ∈ p
16 13 csn class z
17 14 16 cdif class p ∖ z
18 17 cuni class ⋃ p ∖ z
19 15 18 13 cif class if z ∈ p ⋃ p ∖ z z
20 12 5 19 cmpt class z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z
21 3 11 20 cmpt class p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z
22 1 2 21 cmpt class d ∈ V ⟼ p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z
23 0 22 wceq wff pmTrsp = d ∈ V ⟼ p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z