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 
|- T = ( pmTrsp ` D )
Assertion pmtrprfv2 
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` Y ) = X )

Proof

Step Hyp Ref Expression
1 pmtrprfv2.t 
 |-  T = ( pmTrsp ` D )
2 prcom 
 |-  { Y , X } = { X , Y }
3 2 fveq2i 
 |-  ( T ` { Y , X } ) = ( T ` { X , Y } )
4 3 fveq1i 
 |-  ( ( T ` { Y , X } ) ` Y ) = ( ( T ` { X , Y } ) ` Y )
5 ancom 
 |-  ( ( X e. D /\ Y e. D ) <-> ( Y e. D /\ X e. D ) )
6 necom 
 |-  ( X =/= Y <-> Y =/= X )
7 5 6 anbi12i 
 |-  ( ( ( X e. D /\ Y e. D ) /\ X =/= Y ) <-> ( ( Y e. D /\ X e. D ) /\ Y =/= X ) )
8 df-3an 
 |-  ( ( X e. D /\ Y e. D /\ X =/= Y ) <-> ( ( X e. D /\ Y e. D ) /\ X =/= Y ) )
9 df-3an 
 |-  ( ( Y e. D /\ X e. D /\ Y =/= X ) <-> ( ( Y e. D /\ X e. D ) /\ Y =/= X ) )
10 7 8 9 3bitr4i 
 |-  ( ( X e. D /\ Y e. D /\ X =/= Y ) <-> ( Y e. D /\ X e. D /\ Y =/= X ) )
11 1 pmtrprfv 
 |-  ( ( D e. V /\ ( Y e. D /\ X e. D /\ Y =/= X ) ) -> ( ( T ` { Y , X } ) ` Y ) = X )
12 10 11 sylan2b 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { Y , X } ) ` Y ) = X )
13 4 12 eqtr3id 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` Y ) = X )