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

Metamath Proof Explorer

Theorem pmtrfv

Description: General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrfval.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 1 pmtrval ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( 𝑇 ‘ 𝑃 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) )
3 2 fveq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) )
4 3 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) )
5 eqid ⊢ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) )
6 eleq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 ∈ 𝑃 ↔ 𝑍 ∈ 𝑃 ) )
7 sneq ⊢ ( 𝑧 = 𝑍 → { 𝑧 } = { 𝑍 } )
8 7 difeq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑃 ∖ { 𝑧 } ) = ( 𝑃 ∖ { 𝑍 } ) )
9 8 unieqd ⊢ ( 𝑧 = 𝑍 → ∪ ( 𝑃 ∖ { 𝑧 } ) = ∪ ( 𝑃 ∖ { 𝑍 } ) )
10 id ⊢ ( 𝑧 = 𝑍 → 𝑧 = 𝑍 )
11 6 9 10 ifbieq12d ⊢ ( 𝑧 = 𝑍 → if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
12 simpr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → 𝑍 ∈ 𝐷 )
13 simpl3 ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → 𝑃 ≈ 2o )
14 relen ⊢ Rel ≈
15 14 brrelex1i ⊢ ( 𝑃 ≈ 2o → 𝑃 ∈ V )
16 difexg ⊢ ( 𝑃 ∈ V → ( 𝑃 ∖ { 𝑍 } ) ∈ V )
17 uniexg ⊢ ( ( 𝑃 ∖ { 𝑍 } ) ∈ V → ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V )
18 13 15 16 17 4syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V )
19 ifexg ⊢ ( ( ∪ ( 𝑃 ∖ { 𝑍 } ) ∈ V ∧ 𝑍 ∈ 𝐷 ) → if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) ∈ V )
20 18 19 sylancom ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) ∈ V )
21 5 11 12 20 fvmptd3 ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑧 } ) , 𝑧 ) ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
22 4 21 eqtrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )