| Step |
Hyp |
Ref |
Expression |
| 1 |
|
arwrcl.a |
|- A = ( Arrow ` C ) |
| 2 |
|
arwdm.b |
|- B = ( Base ` C ) |
| 3 |
|
fo1st |
|- 1st : _V -onto-> _V |
| 4 |
|
fofn |
|- ( 1st : _V -onto-> _V -> 1st Fn _V ) |
| 5 |
3 4
|
ax-mp |
|- 1st Fn _V |
| 6 |
|
fof |
|- ( 1st : _V -onto-> _V -> 1st : _V --> _V ) |
| 7 |
3 6
|
ax-mp |
|- 1st : _V --> _V |
| 8 |
|
fnfco |
|- ( ( 1st Fn _V /\ 1st : _V --> _V ) -> ( 1st o. 1st ) Fn _V ) |
| 9 |
5 7 8
|
mp2an |
|- ( 1st o. 1st ) Fn _V |
| 10 |
|
df-doma |
|- domA = ( 1st o. 1st ) |
| 11 |
10
|
fneq1i |
|- ( domA Fn _V <-> ( 1st o. 1st ) Fn _V ) |
| 12 |
9 11
|
mpbir |
|- domA Fn _V |
| 13 |
|
ssv |
|- A C_ _V |
| 14 |
|
fnssres |
|- ( ( domA Fn _V /\ A C_ _V ) -> ( domA |` A ) Fn A ) |
| 15 |
12 13 14
|
mp2an |
|- ( domA |` A ) Fn A |
| 16 |
|
fvres |
|- ( x e. A -> ( ( domA |` A ) ` x ) = ( domA ` x ) ) |
| 17 |
1 2
|
arwdm |
|- ( x e. A -> ( domA ` x ) e. B ) |
| 18 |
16 17
|
eqeltrd |
|- ( x e. A -> ( ( domA |` A ) ` x ) e. B ) |
| 19 |
18
|
rgen |
|- A. x e. A ( ( domA |` A ) ` x ) e. B |
| 20 |
|
ffnfv |
|- ( ( domA |` A ) : A --> B <-> ( ( domA |` A ) Fn A /\ A. x e. A ( ( domA |` A ) ` x ) e. B ) ) |
| 21 |
15 19 20
|
mpbir2an |
|- ( domA |` A ) : A --> B |