Metamath Proof Explorer

Theorem pmtrval

Description: A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Hypothesis pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrval ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 1 pmtrfval ⊢ ( 𝐷 ∈ 𝑉 → 𝑇 = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
3 2 fveq1d ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑇 ‘ 𝑃 ) = ( ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ‘ 𝑃 ) )
4 3 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ‘ 𝑃 ) )
5 eqid ⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
6 eleq2 ⊢ ( 𝑝 = 𝑃 → ( 𝑧 ∈ 𝑝 ↔ 𝑧 ∈ 𝑃 ) )
7 difeq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∖ { 𝑧 } ) = ( 𝑃 ∖ { 𝑧 } ) )
8 7 unieqd ⊢ ( 𝑝 = 𝑃 → ∪ ( 𝑝 ∖ { 𝑧 } ) = ∪ ( 𝑃 ∖ { 𝑧 } ) )
9 6 8 ifbieq1d ⊢ ( 𝑝 = 𝑃 → if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) = if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) )
10 9 mpteq2dv ⊢ ( 𝑝 = 𝑃 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )
11 breq1 ⊢ ( 𝑦 = 𝑃 → ( 𝑦 ≈ 2o ↔ 𝑃 ≈ 2o ) )
12 elpw2g ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ∈ 𝒫 𝐷 ↔ 𝑃 ⊆ 𝐷 ) )
13 12 biimpar ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ) → 𝑃 ∈ 𝒫 𝐷 )
14 13 3adant3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ 𝒫 𝐷 )
15 simp3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ≈ 2o )
16 11 14 15 elrabd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → 𝑃 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } )
17 mptexg ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V )
18 17 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ∈ V )
19 5 10 16 18 fvmptd3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )
20 4 19 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )