Metamath Proof Explorer

Theorem pmtrprfv3

Description: In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019)

Ref Expression
Hypothesis pmtrfval.t 
|- T = ( pmTrsp ` D )
Assertion pmtrprfv3 
|- ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = Z )

Proof

Step Hyp Ref Expression
1 pmtrfval.t 
 |-  T = ( pmTrsp ` D )
2 simp1 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> D e. V )
3 simp1 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> X e. D )
4 3 3ad2ant2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> X e. D )
5 simp22 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Y e. D )
6 4 5 prssd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } C_ D )
7 enpr2 
 |-  ( ( X e. D /\ Y e. D /\ X =/= Y ) -> { X , Y } ~~ 2o )
8 7 3expia 
 |-  ( ( X e. D /\ Y e. D ) -> ( X =/= Y -> { X , Y } ~~ 2o ) )
9 8 3adant3 
 |-  ( ( X e. D /\ Y e. D /\ Z e. D ) -> ( X =/= Y -> { X , Y } ~~ 2o ) )
10 9 com12 
 |-  ( X =/= Y -> ( ( X e. D /\ Y e. D /\ Z e. D ) -> { X , Y } ~~ 2o ) )
11 10 3ad2ant1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( ( X e. D /\ Y e. D /\ Z e. D ) -> { X , Y } ~~ 2o ) )
12 11 impcom 
 |-  ( ( ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } ~~ 2o )
13 12 3adant1 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> { X , Y } ~~ 2o )
14 simp23 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z e. D )
15 1 pmtrfv 
 |-  ( ( ( D e. V /\ { X , Y } C_ D /\ { X , Y } ~~ 2o ) /\ Z e. D ) -> ( ( T ` { X , Y } ) ` Z ) = if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) )
16 2 6 13 14 15 syl31anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) )
17 necom 
 |-  ( X =/= Z <-> Z =/= X )
18 17 biimpi 
 |-  ( X =/= Z -> Z =/= X )
19 18 3ad2ant2 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Z =/= X )
20 19 3ad2ant3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z =/= X )
21 necom 
 |-  ( Y =/= Z <-> Z =/= Y )
22 21 biimpi 
 |-  ( Y =/= Z -> Z =/= Y )
23 22 3ad2ant3 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> Z =/= Y )
24 23 3ad2ant3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> Z =/= Y )
25 20 24 nelprd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> -. Z e. { X , Y } )
26 25 iffalsed 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> if ( Z e. { X , Y } , U. ( { X , Y } \ { Z } ) , Z ) = Z )
27 16 26 eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ Z e. D ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( T ` { X , Y } ) ` Z ) = Z )