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

Metamath Proof Explorer

Theorem pmtrprfv2

Description: In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypothesis pmtrprfv2.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrprfv2 ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 pmtrprfv2.t ⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2 prcom ⊢ { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
3 2 fveq2i ⊢ ( 𝑇 ‘ { 𝑌 , 𝑋 } ) = ( 𝑇 ‘ { 𝑋 , 𝑌 } )
4 3 fveq1i ⊢ ( ( 𝑇 ‘ { 𝑌 , 𝑋 } ) ‘ 𝑌 ) = ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 )
5 ancom ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) )
6 necom ⊢ ( 𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋 )
7 5 6 anbi12i ⊢ ( ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) ∧ 𝑌 ≠ 𝑋 ) )
8 df-3an ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ) ∧ 𝑋 ≠ 𝑌 ) )
9 df-3an ⊢ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ∧ 𝑌 ≠ 𝑋 ) ↔ ( ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ) ∧ 𝑌 ≠ 𝑋 ) )
10 7 8 9 3bitr4i ⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ∧ 𝑌 ≠ 𝑋 ) )
11 1 pmtrprfv ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝐷 ∧ 𝑋 ∈ 𝐷 ∧ 𝑌 ≠ 𝑋 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑋 } ) ‘ 𝑌 ) = 𝑋 )
12 10 11 sylan2b ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑌 , 𝑋 } ) ‘ 𝑌 ) = 𝑋 )
13 4 12 eqtr3id ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )