| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mapcod.1 |
|- ( ph -> F e. ( A ^m B ) ) |
| 2 |
|
mapcod.2 |
|- ( ph -> G e. ( B ^m C ) ) |
| 3 |
|
elmapex |
|- ( F e. ( A ^m B ) -> ( A e. _V /\ B e. _V ) ) |
| 4 |
1 3
|
syl |
|- ( ph -> ( A e. _V /\ B e. _V ) ) |
| 5 |
4
|
simpld |
|- ( ph -> A e. _V ) |
| 6 |
|
elmapex |
|- ( G e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) ) |
| 7 |
2 6
|
syl |
|- ( ph -> ( B e. _V /\ C e. _V ) ) |
| 8 |
7
|
simprd |
|- ( ph -> C e. _V ) |
| 9 |
|
elmapi |
|- ( F e. ( A ^m B ) -> F : B --> A ) |
| 10 |
1 9
|
syl |
|- ( ph -> F : B --> A ) |
| 11 |
|
elmapi |
|- ( G e. ( B ^m C ) -> G : C --> B ) |
| 12 |
2 11
|
syl |
|- ( ph -> G : C --> B ) |
| 13 |
10 12
|
fcod |
|- ( ph -> ( F o. G ) : C --> A ) |
| 14 |
5 8 13
|
elmapdd |
|- ( ph -> ( F o. G ) e. ( A ^m C ) ) |