Step |
Hyp |
Ref |
Expression |
1 |
|
releldm2 |
|- ( Rel A -> ( y e. dom A <-> E. z e. A ( 1st ` z ) = y ) ) |
2 |
|
fvex |
|- ( 1st ` x ) e. _V |
3 |
|
eqid |
|- ( x e. A |-> ( 1st ` x ) ) = ( x e. A |-> ( 1st ` x ) ) |
4 |
2 3
|
fnmpti |
|- ( x e. A |-> ( 1st ` x ) ) Fn A |
5 |
|
fvelrnb |
|- ( ( x e. A |-> ( 1st ` x ) ) Fn A -> ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y ) ) |
6 |
4 5
|
ax-mp |
|- ( y e. ran ( x e. A |-> ( 1st ` x ) ) <-> E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y ) |
7 |
|
fveq2 |
|- ( x = z -> ( 1st ` x ) = ( 1st ` z ) ) |
8 |
|
fvex |
|- ( 1st ` z ) e. _V |
9 |
7 3 8
|
fvmpt |
|- ( z e. A -> ( ( x e. A |-> ( 1st ` x ) ) ` z ) = ( 1st ` z ) ) |
10 |
9
|
eqeq1d |
|- ( z e. A -> ( ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> ( 1st ` z ) = y ) ) |
11 |
10
|
rexbiia |
|- ( E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> E. z e. A ( 1st ` z ) = y ) |
12 |
11
|
a1i |
|- ( Rel A -> ( E. z e. A ( ( x e. A |-> ( 1st ` x ) ) ` z ) = y <-> E. z e. A ( 1st ` z ) = y ) ) |
13 |
6 12
|
bitr2id |
|- ( Rel A -> ( E. z e. A ( 1st ` z ) = y <-> y e. ran ( x e. A |-> ( 1st ` x ) ) ) ) |
14 |
1 13
|
bitrd |
|- ( Rel A -> ( y e. dom A <-> y e. ran ( x e. A |-> ( 1st ` x ) ) ) ) |
15 |
14
|
eqrdv |
|- ( Rel A -> dom A = ran ( x e. A |-> ( 1st ` x ) ) ) |