| Step |
Hyp |
Ref |
Expression |
| 1 |
|
functermc.d |
|- ( ph -> D e. Cat ) |
| 2 |
|
functermc.e |
|- ( ph -> E e. TermCat ) |
| 3 |
|
functermc.b |
|- B = ( Base ` D ) |
| 4 |
|
functermc.c |
|- C = ( Base ` E ) |
| 5 |
|
functermc.h |
|- H = ( Hom ` D ) |
| 6 |
|
functermc.j |
|- J = ( Hom ` E ) |
| 7 |
|
functermc.f |
|- F = ( B X. C ) |
| 8 |
|
functermc.g |
|- G = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) |
| 9 |
|
relfunc |
|- Rel ( D Func E ) |
| 10 |
3
|
fvexi |
|- B e. _V |
| 11 |
4
|
fvexi |
|- C e. _V |
| 12 |
10 11
|
xpex |
|- ( B X. C ) e. _V |
| 13 |
7 12
|
eqeltri |
|- F e. _V |
| 14 |
10 10
|
mpoex |
|- ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) e. _V |
| 15 |
8 14
|
eqeltri |
|- G e. _V |
| 16 |
13 15
|
relsnop |
|- Rel { <. F , G >. } |
| 17 |
1 2 3 4 5 6 7 8
|
functermc |
|- ( ph -> ( z ( D Func E ) w <-> ( z = F /\ w = G ) ) ) |
| 18 |
|
brsnop |
|- ( ( F e. _V /\ G e. _V ) -> ( z { <. F , G >. } w <-> ( z = F /\ w = G ) ) ) |
| 19 |
13 15 18
|
mp2an |
|- ( z { <. F , G >. } w <-> ( z = F /\ w = G ) ) |
| 20 |
17 19
|
bitr4di |
|- ( ph -> ( z ( D Func E ) w <-> z { <. F , G >. } w ) ) |
| 21 |
9 16 20
|
eqbrrdiv |
|- ( ph -> ( D Func E ) = { <. F , G >. } ) |