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