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