Step |
Hyp |
Ref |
Expression |
1 |
|
funcid.b |
|- B = ( Base ` D ) |
2 |
|
funcid.1 |
|- .1. = ( Id ` D ) |
3 |
|
funcid.i |
|- I = ( Id ` E ) |
4 |
|
funcid.f |
|- ( ph -> F ( D Func E ) G ) |
5 |
|
funcid.x |
|- ( ph -> X e. B ) |
6 |
|
id |
|- ( x = X -> x = X ) |
7 |
6 6
|
oveq12d |
|- ( x = X -> ( x G x ) = ( X G X ) ) |
8 |
|
fveq2 |
|- ( x = X -> ( .1. ` x ) = ( .1. ` X ) ) |
9 |
7 8
|
fveq12d |
|- ( x = X -> ( ( x G x ) ` ( .1. ` x ) ) = ( ( X G X ) ` ( .1. ` X ) ) ) |
10 |
|
2fveq3 |
|- ( x = X -> ( I ` ( F ` x ) ) = ( I ` ( F ` X ) ) ) |
11 |
9 10
|
eqeq12d |
|- ( x = X -> ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) <-> ( ( X G X ) ` ( .1. ` X ) ) = ( I ` ( F ` X ) ) ) ) |
12 |
|
eqid |
|- ( Base ` E ) = ( Base ` E ) |
13 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
14 |
|
eqid |
|- ( Hom ` E ) = ( Hom ` E ) |
15 |
|
eqid |
|- ( comp ` D ) = ( comp ` D ) |
16 |
|
eqid |
|- ( comp ` E ) = ( comp ` E ) |
17 |
|
df-br |
|- ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) ) |
18 |
4 17
|
sylib |
|- ( ph -> <. F , G >. e. ( D Func E ) ) |
19 |
|
funcrcl |
|- ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) ) |
20 |
18 19
|
syl |
|- ( ph -> ( D e. Cat /\ E e. Cat ) ) |
21 |
20
|
simpld |
|- ( ph -> D e. Cat ) |
22 |
20
|
simprd |
|- ( ph -> E e. Cat ) |
23 |
1 12 13 14 2 3 15 16 21 22
|
isfunc |
|- ( ph -> ( F ( D Func E ) G <-> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` D ) ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) ) |
24 |
4 23
|
mpbid |
|- ( ph -> ( F : B --> ( Base ` E ) /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` D ) ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) |
25 |
24
|
simp3d |
|- ( ph -> A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) |
26 |
|
simpl |
|- ( ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) -> ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) |
27 |
26
|
ralimi |
|- ( A. x e. B ( ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) -> A. x e. B ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) |
28 |
25 27
|
syl |
|- ( ph -> A. x e. B ( ( x G x ) ` ( .1. ` x ) ) = ( I ` ( F ` x ) ) ) |
29 |
11 28 5
|
rspcdva |
|- ( ph -> ( ( X G X ) ` ( .1. ` X ) ) = ( I ` ( F ` X ) ) ) |