Metamath Proof Explorer

Theorem pmtrfval

Description: The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢T=pmTrsp⁡D
Assertion pmtrfval ⊢D∈V→T=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢T=pmTrsp⁡D
2 elex ⊢D∈V→D∈V
3 pweq ⊢d=D→𝒫d=𝒫D
4 3 rabeqdv ⊢d=D→y∈𝒫d|y≈2𝑜=y∈𝒫D|y≈2𝑜
5 mpteq1 ⊢d=D→z∈d⟼ifz∈p⋃p∖zz=z∈D⟼ifz∈p⋃p∖zz
6 4 5 mpteq12dv ⊢d=D→p∈y∈𝒫d|y≈2𝑜⟼z∈d⟼ifz∈p⋃p∖zz=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz
7 df-pmtr ⊢pmTrsp=d∈V⟼p∈y∈𝒫d|y≈2𝑜⟼z∈d⟼ifz∈p⋃p∖zz
8 vpwex ⊢𝒫d∈V
9 8 mptrabex ⊢p∈y∈𝒫d|y≈2𝑜⟼z∈d⟼ifz∈p⋃p∖zz∈V
10 6 7 9 fvmpt3i ⊢D∈V→pmTrsp⁡D=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz
11 2 10 syl ⊢D∈V→pmTrsp⁡D=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz
12 1 11 eqtrid ⊢D∈V→T=p∈y∈𝒫D|y≈2𝑜⟼z∈D⟼ifz∈p⋃p∖zz