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 >. } }