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	⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )