Metamath Proof Explorer

Theorem pmtrprfval

Description: The transpositions on a pair. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pmtrprfval 
|- ( pmTrsp ` { 1 , 2 } ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )

Proof

Step Hyp Ref Expression
1 prex 
 |-  { 1 , 2 } e. _V
2 eqid 
 |-  ( pmTrsp ` { 1 , 2 } ) = ( pmTrsp ` { 1 , 2 } )
3 2 pmtrfval 
 |-  ( { 1 , 2 } e. _V -> ( pmTrsp ` { 1 , 2 } ) = ( p e. { t e. ~P { 1 , 2 } | t ~~ 2o } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
4 1 3 ax-mp 
 |-  ( pmTrsp ` { 1 , 2 } ) = ( p e. { t e. ~P { 1 , 2 } | t ~~ 2o } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
5 1ex 
 |-  1 e. _V
6 2nn0 
 |-  2 e. NN0
7 1ne2 
 |-  1 =/= 2
8 pr2pwpr 
 |-  ( ( 1 e. _V /\ 2 e. NN0 /\ 1 =/= 2 ) -> { t e. ~P { 1 , 2 } | t ~~ 2o } = { { 1 , 2 } } )
9 5 6 7 8 mp3an 
 |-  { t e. ~P { 1 , 2 } | t ~~ 2o } = { { 1 , 2 } }
10 9 mpteq1i 
 |-  ( p e. { t e. ~P { 1 , 2 } | t ~~ 2o } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
11 elsni 
 |-  ( p e. { { 1 , 2 } } -> p = { 1 , 2 } )
12 eleq2 
 |-  ( p = { 1 , 2 } -> ( z e. p <-> z e. { 1 , 2 } ) )
13 12 biimpar 
 |-  ( ( p = { 1 , 2 } /\ z e. { 1 , 2 } ) -> z e. p )
14 13 iftrued 
 |-  ( ( p = { 1 , 2 } /\ z e. { 1 , 2 } ) -> if ( z e. p , U. ( p \ { z } ) , z ) = U. ( p \ { z } ) )
15 elpri 
 |-  ( z e. { 1 , 2 } -> ( z = 1 \/ z = 2 ) )
16 2ex 
 |-  2 e. _V
17 16 unisn 
 |-  U. { 2 } = 2
18 simpr 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> p = { 1 , 2 } )
19 sneq 
 |-  ( z = 1 -> { z } = { 1 } )
20 19 adantr 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> { z } = { 1 } )
21 18 20 difeq12d 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> ( p \ { z } ) = ( { 1 , 2 } \ { 1 } ) )
22 difprsn1 
 |-  ( 1 =/= 2 -> ( { 1 , 2 } \ { 1 } ) = { 2 } )
23 7 22 ax-mp 
 |-  ( { 1 , 2 } \ { 1 } ) = { 2 }
24 21 23 eqtrdi 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> ( p \ { z } ) = { 2 } )
25 24 unieqd 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> U. ( p \ { z } ) = U. { 2 } )
26 iftrue 
 |-  ( z = 1 -> if ( z = 1 , 2 , 1 ) = 2 )
27 26 adantr 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> if ( z = 1 , 2 , 1 ) = 2 )
28 17 25 27 3eqtr4a 
 |-  ( ( z = 1 /\ p = { 1 , 2 } ) -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) )
29 28 ex 
 |-  ( z = 1 -> ( p = { 1 , 2 } -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) ) )
30 5 unisn 
 |-  U. { 1 } = 1
31 simpr 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> p = { 1 , 2 } )
32 sneq 
 |-  ( z = 2 -> { z } = { 2 } )
33 32 adantr 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> { z } = { 2 } )
34 31 33 difeq12d 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> ( p \ { z } ) = ( { 1 , 2 } \ { 2 } ) )
35 difprsn2 
 |-  ( 1 =/= 2 -> ( { 1 , 2 } \ { 2 } ) = { 1 } )
36 7 35 ax-mp 
 |-  ( { 1 , 2 } \ { 2 } ) = { 1 }
37 34 36 eqtrdi 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> ( p \ { z } ) = { 1 } )
38 37 unieqd 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> U. ( p \ { z } ) = U. { 1 } )
39 7 nesymi 
 |-  -. 2 = 1
40 eqeq1 
 |-  ( z = 2 -> ( z = 1 <-> 2 = 1 ) )
41 39 40 mtbiri 
 |-  ( z = 2 -> -. z = 1 )
42 41 iffalsed 
 |-  ( z = 2 -> if ( z = 1 , 2 , 1 ) = 1 )
43 42 adantr 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> if ( z = 1 , 2 , 1 ) = 1 )
44 30 38 43 3eqtr4a 
 |-  ( ( z = 2 /\ p = { 1 , 2 } ) -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) )
45 44 ex 
 |-  ( z = 2 -> ( p = { 1 , 2 } -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) ) )
46 29 45 jaoi 
 |-  ( ( z = 1 \/ z = 2 ) -> ( p = { 1 , 2 } -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) ) )
47 15 46 syl 
 |-  ( z e. { 1 , 2 } -> ( p = { 1 , 2 } -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) ) )
48 47 impcom 
 |-  ( ( p = { 1 , 2 } /\ z e. { 1 , 2 } ) -> U. ( p \ { z } ) = if ( z = 1 , 2 , 1 ) )
49 14 48 eqtrd 
 |-  ( ( p = { 1 , 2 } /\ z e. { 1 , 2 } ) -> if ( z e. p , U. ( p \ { z } ) , z ) = if ( z = 1 , 2 , 1 ) )
50 11 49 sylan 
 |-  ( ( p e. { { 1 , 2 } } /\ z e. { 1 , 2 } ) -> if ( z e. p , U. ( p \ { z } ) , z ) = if ( z = 1 , 2 , 1 ) )
51 50 mpteq2dva 
 |-  ( p e. { { 1 , 2 } } -> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
52 51 mpteq2ia 
 |-  ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
53 10 52 eqtri 
 |-  ( p e. { t e. ~P { 1 , 2 } | t ~~ 2o } |-> ( z e. { 1 , 2 } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
54 4 53 eqtri 
 |-  ( pmTrsp ` { 1 , 2 } ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )