Metamath Proof Explorer

Theorem pmtrprfvalrn

Description: The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pmtrprfvalrn 
|- ran ( pmTrsp ` { 1 , 2 } ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }

Proof

Step Hyp Ref Expression
1 pmtrprfval 
 |-  ( pmTrsp ` { 1 , 2 } ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
2 1 rneqi 
 |-  ran ( pmTrsp ` { 1 , 2 } ) = ran ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
3 eqid 
 |-  ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) ) = ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
4 3 rnmpt 
 |-  ran ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) ) = { t | E. p e. { { 1 , 2 } } t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) }
5 1ex 
 |-  1 e. _V
6 id 
 |-  ( 1 e. _V -> 1 e. _V )
7 2nn 
 |-  2 e. NN
8 7 a1i 
 |-  ( 1 e. _V -> 2 e. NN )
9 iftrue 
 |-  ( z = 1 -> if ( z = 1 , 2 , 1 ) = 2 )
10 9 adantl 
 |-  ( ( 1 e. _V /\ z = 1 ) -> if ( z = 1 , 2 , 1 ) = 2 )
11 1ne2 
 |-  1 =/= 2
12 11 nesymi 
 |-  -. 2 = 1
13 eqeq1 
 |-  ( z = 2 -> ( z = 1 <-> 2 = 1 ) )
14 12 13 mtbiri 
 |-  ( z = 2 -> -. z = 1 )
15 14 iffalsed 
 |-  ( z = 2 -> if ( z = 1 , 2 , 1 ) = 1 )
16 15 adantl 
 |-  ( ( 1 e. _V /\ z = 2 ) -> if ( z = 1 , 2 , 1 ) = 1 )
17 6 8 8 6 10 16 fmptpr 
 |-  ( 1 e. _V -> { <. 1 , 2 >. , <. 2 , 1 >. } = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
18 17 eqeq2d 
 |-  ( 1 e. _V -> ( t = { <. 1 , 2 >. , <. 2 , 1 >. } <-> t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) ) )
19 5 18 ax-mp 
 |-  ( t = { <. 1 , 2 >. , <. 2 , 1 >. } <-> t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) )
20 19 bicomi 
 |-  ( t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) <-> t = { <. 1 , 2 >. , <. 2 , 1 >. } )
21 20 rexbii 
 |-  ( E. p e. { { 1 , 2 } } t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) <-> E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } )
22 21 abbii 
 |-  { t | E. p e. { { 1 , 2 } } t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) } = { t | E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } }
23 prex 
 |-  { 1 , 2 } e. _V
24 23 snnz 
 |-  { { 1 , 2 } } =/= (/)
25 r19.9rzv 
 |-  ( { { 1 , 2 } } =/= (/) -> ( s = { <. 1 , 2 >. , <. 2 , 1 >. } <-> E. p e. { { 1 , 2 } } s = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
26 25 bicomd 
 |-  ( { { 1 , 2 } } =/= (/) -> ( E. p e. { { 1 , 2 } } s = { <. 1 , 2 >. , <. 2 , 1 >. } <-> s = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
27 24 26 ax-mp 
 |-  ( E. p e. { { 1 , 2 } } s = { <. 1 , 2 >. , <. 2 , 1 >. } <-> s = { <. 1 , 2 >. , <. 2 , 1 >. } )
28 vex 
 |-  s e. _V
29 eqeq1 
 |-  ( t = s -> ( t = { <. 1 , 2 >. , <. 2 , 1 >. } <-> s = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
30 29 rexbidv 
 |-  ( t = s -> ( E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } <-> E. p e. { { 1 , 2 } } s = { <. 1 , 2 >. , <. 2 , 1 >. } ) )
31 28 30 elab 
 |-  ( s e. { t | E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } } <-> E. p e. { { 1 , 2 } } s = { <. 1 , 2 >. , <. 2 , 1 >. } )
32 velsn 
 |-  ( s e. { { <. 1 , 2 >. , <. 2 , 1 >. } } <-> s = { <. 1 , 2 >. , <. 2 , 1 >. } )
33 27 31 32 3bitr4i 
 |-  ( s e. { t | E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } } <-> s e. { { <. 1 , 2 >. , <. 2 , 1 >. } } )
34 33 eqriv 
 |-  { t | E. p e. { { 1 , 2 } } t = { <. 1 , 2 >. , <. 2 , 1 >. } } = { { <. 1 , 2 >. , <. 2 , 1 >. } }
35 22 34 eqtri 
 |-  { t | E. p e. { { 1 , 2 } } t = ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) } = { { <. 1 , 2 >. , <. 2 , 1 >. } }
36 4 35 eqtri 
 |-  ran ( p e. { { 1 , 2 } } |-> ( z e. { 1 , 2 } |-> if ( z = 1 , 2 , 1 ) ) ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }
37 2 36 eqtri 
 |-  ran ( pmTrsp ` { 1 , 2 } ) = { { <. 1 , 2 >. , <. 2 , 1 >. } }