Step |
Hyp |
Ref |
Expression |
1 |
|
vafval.2 |
|- G = ( +v ` U ) |
2 |
|
df-va |
|- +v = ( 1st o. 1st ) |
3 |
2
|
fveq1i |
|- ( +v ` U ) = ( ( 1st o. 1st ) ` U ) |
4 |
|
fo1st |
|- 1st : _V -onto-> _V |
5 |
|
fof |
|- ( 1st : _V -onto-> _V -> 1st : _V --> _V ) |
6 |
4 5
|
ax-mp |
|- 1st : _V --> _V |
7 |
|
fvco3 |
|- ( ( 1st : _V --> _V /\ U e. _V ) -> ( ( 1st o. 1st ) ` U ) = ( 1st ` ( 1st ` U ) ) ) |
8 |
6 7
|
mpan |
|- ( U e. _V -> ( ( 1st o. 1st ) ` U ) = ( 1st ` ( 1st ` U ) ) ) |
9 |
3 8
|
syl5eq |
|- ( U e. _V -> ( +v ` U ) = ( 1st ` ( 1st ` U ) ) ) |
10 |
|
fvprc |
|- ( -. U e. _V -> ( +v ` U ) = (/) ) |
11 |
|
fvprc |
|- ( -. U e. _V -> ( 1st ` U ) = (/) ) |
12 |
11
|
fveq2d |
|- ( -. U e. _V -> ( 1st ` ( 1st ` U ) ) = ( 1st ` (/) ) ) |
13 |
|
1st0 |
|- ( 1st ` (/) ) = (/) |
14 |
12 13
|
eqtr2di |
|- ( -. U e. _V -> (/) = ( 1st ` ( 1st ` U ) ) ) |
15 |
10 14
|
eqtrd |
|- ( -. U e. _V -> ( +v ` U ) = ( 1st ` ( 1st ` U ) ) ) |
16 |
9 15
|
pm2.61i |
|- ( +v ` U ) = ( 1st ` ( 1st ` U ) ) |
17 |
1 16
|
eqtri |
|- G = ( 1st ` ( 1st ` U ) ) |