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