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

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 ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrfval ( 𝐷 ∈ 𝑉 → 𝑇 = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 elex ⊢ ( 𝐷 ∈ 𝑉 → 𝐷 ∈ V )
3 pweq ⊢ ( 𝑑 = 𝐷 → 𝒫 𝑑 = 𝒫 𝐷 )
4 3 rabeqdv ⊢ ( 𝑑 = 𝐷 → { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } = { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } )
5 mpteq1 ⊢ ( 𝑑 = 𝐷 → ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
6 4 5 mpteq12dv ⊢ ( 𝑑 = 𝐷 → ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
7 df-pmtr ⊢ pmTrsp = ( 𝑑 ∈ V ↦ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
8 vpwex ⊢ 𝒫 𝑑 ∈ V
9 8 mptrabex ⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝑑 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∈ V
10 6 7 9 fvmpt3i ⊢ ( 𝐷 ∈ V → ( pmTrsp ‘ 𝐷 ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
11 2 10 syl ⊢ ( 𝐷 ∈ 𝑉 → ( pmTrsp ‘ 𝐷 ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
12 1 11 eqtrid ⊢ ( 𝐷 ∈ 𝑉 → 𝑇 = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )