Metamath Proof Explorer

Theorem pmtrprfv

Description: In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 pmtrfval.t 
 |-  T = ( pmTrsp ` D )
2 simpl 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> D e. V )
3 simpr1 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> X e. D )
4 simpr2 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> Y e. D )
5 3 4 prssd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> { X , Y } C_ D )
6 pr2nelem 
 |-  ( ( X e. D /\ Y e. D /\ X =/= Y ) -> { X , Y } ~~ 2o )
7 6 adantl 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> { X , Y } ~~ 2o )
8 1 pmtrfv 
 |-  ( ( ( D e. V /\ { X , Y } C_ D /\ { X , Y } ~~ 2o ) /\ X e. D ) -> ( ( T ` { X , Y } ) ` X ) = if ( X e. { X , Y } , U. ( { X , Y } \ { X } ) , X ) )
9 2 5 7 3 8 syl31anc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` X ) = if ( X e. { X , Y } , U. ( { X , Y } \ { X } ) , X ) )
10 prid1g 
 |-  ( X e. D -> X e. { X , Y } )
11 3 10 syl 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> X e. { X , Y } )
12 11 iftrued 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> if ( X e. { X , Y } , U. ( { X , Y } \ { X } ) , X ) = U. ( { X , Y } \ { X } ) )
13 difprsnss 
 |-  ( { X , Y } \ { X } ) C_ { Y }
14 13 a1i 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( { X , Y } \ { X } ) C_ { Y } )
15 prid2g 
 |-  ( Y e. D -> Y e. { X , Y } )
16 4 15 syl 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> Y e. { X , Y } )
17 simpr3 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> X =/= Y )
18 17 necomd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> Y =/= X )
19 eldifsn 
 |-  ( Y e. ( { X , Y } \ { X } ) <-> ( Y e. { X , Y } /\ Y =/= X ) )
20 16 18 19 sylanbrc 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> Y e. ( { X , Y } \ { X } ) )
21 20 snssd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> { Y } C_ ( { X , Y } \ { X } ) )
22 14 21 eqssd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( { X , Y } \ { X } ) = { Y } )
23 22 unieqd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> U. ( { X , Y } \ { X } ) = U. { Y } )
24 unisng 
 |-  ( Y e. D -> U. { Y } = Y )
25 4 24 syl 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> U. { Y } = Y )
26 23 25 eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> U. ( { X , Y } \ { X } ) = Y )
27 12 26 eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> if ( X e. { X , Y } , U. ( { X , Y } \ { X } ) , X ) = Y )
28 9 27 eqtrd 
 |-  ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` X ) = Y )