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 = ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpmtr ⊢ pmTrsp
1 vd ⊢ 𝑑
2 cvv ⊢ V
3 vp ⊢ 𝑝
4 vy ⊢ 𝑦
5 1 cv ⊢ 𝑑
6 5 cpw ⊢ 𝒫 𝑑
7 4 cv ⊢ 𝑦
8 cen ⊢ ≈
9 c2o ⊢ 2o
10 7 9 8 wbr ⊢ 𝑦 ≈ 2o
11 10 4 6 crab ⊢ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o }
12 vz ⊢ 𝑧
13 12 cv ⊢ 𝑧
14 3 cv ⊢ 𝑝
15 13 14 wcel ⊢ 𝑧 ∈ 𝑝
16 13 csn ⊢ { 𝑧 }
17 14 16 cdif ⊢ ( 𝑝 ∖ { 𝑧 } )
18 17 cuni ⊢ ∪ ( 𝑝 ∖ { 𝑧 } )
19 15 18 13 cif ⊢ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 )
20 12 5 19 cmpt ⊢ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) )
21 3 11 20 cmpt ⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
22 1 2 21 cmpt ⊢ ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
23 0 22 wceq ⊢ pmTrsp = ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )