| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fo1st |
|- 1st : _V -onto-> _V |
| 2 |
|
fofn |
|- ( 1st : _V -onto-> _V -> 1st Fn _V ) |
| 3 |
1 2
|
ax-mp |
|- 1st Fn _V |
| 4 |
|
dffn5 |
|- ( 1st Fn _V <-> 1st = ( w e. _V |-> ( 1st ` w ) ) ) |
| 5 |
3 4
|
mpbi |
|- 1st = ( w e. _V |-> ( 1st ` w ) ) |
| 6 |
|
mptv |
|- ( w e. _V |-> ( 1st ` w ) ) = { <. w , z >. | z = ( 1st ` w ) } |
| 7 |
5 6
|
eqtri |
|- 1st = { <. w , z >. | z = ( 1st ` w ) } |
| 8 |
7
|
reseq1i |
|- ( 1st |` ( _V X. _V ) ) = ( { <. w , z >. | z = ( 1st ` w ) } |` ( _V X. _V ) ) |
| 9 |
|
resopab |
|- ( { <. w , z >. | z = ( 1st ` w ) } |` ( _V X. _V ) ) = { <. w , z >. | ( w e. ( _V X. _V ) /\ z = ( 1st ` w ) ) } |
| 10 |
|
vex |
|- x e. _V |
| 11 |
|
vex |
|- y e. _V |
| 12 |
10 11
|
op1std |
|- ( w = <. x , y >. -> ( 1st ` w ) = x ) |
| 13 |
12
|
eqeq2d |
|- ( w = <. x , y >. -> ( z = ( 1st ` w ) <-> z = x ) ) |
| 14 |
13
|
dfoprab3 |
|- { <. w , z >. | ( w e. ( _V X. _V ) /\ z = ( 1st ` w ) ) } = { <. <. x , y >. , z >. | z = x } |
| 15 |
8 9 14
|
3eqtrri |
|- { <. <. x , y >. , z >. | z = x } = ( 1st |` ( _V X. _V ) ) |