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 ⟼ if z ∈ p ⋃ p ∖ z z

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 ⟼ if z ∈ p ⋃ p ∖ z z = z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
6 4 5 mpteq12dv ⊢ d = D → p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
7 df-pmtr ⊢ pmTrsp = d ∈ V ⟼ p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z
8 vpwex ⊢ 𝒫 d ∈ V
9 8 mptrabex ⊢ p ∈ y ∈ 𝒫 d | y ≈ 2 𝑜 ⟼ z ∈ d ⟼ if z ∈ p ⋃ p ∖ z z ∈ V
10 6 7 9 fvmpt3i ⊢ D ∈ V → pmTrsp ⁡ D = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
11 2 10 syl ⊢ D ∈ V → pmTrsp ⁡ D = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z
12 1 11 syl5eq ⊢ D ∈ V → T = p ∈ y ∈ 𝒫 D | y ≈ 2 𝑜 ⟼ z ∈ D ⟼ if z ∈ p ⋃ p ∖ z z