Step |
Hyp |
Ref |
Expression |
1 |
|
relfunc |
|- Rel ( C Func ( D |`cat R ) ) |
2 |
1
|
a1i |
|- ( R e. ( Subcat ` D ) -> Rel ( C Func ( D |`cat R ) ) ) |
3 |
|
simpr |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f ( C Func ( D |`cat R ) ) g ) |
4 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
5 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
6 |
|
simpl |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R e. ( Subcat ` D ) ) |
7 |
|
eqidd |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R = dom dom R ) |
8 |
6 7
|
subcfn |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R Fn ( dom dom R X. dom dom R ) ) |
9 |
|
eqid |
|- ( Base ` ( D |`cat R ) ) = ( Base ` ( D |`cat R ) ) |
10 |
4 9 3
|
funcf1 |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f : ( Base ` C ) --> ( Base ` ( D |`cat R ) ) ) |
11 |
|
eqid |
|- ( D |`cat R ) = ( D |`cat R ) |
12 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
13 |
|
subcrcl |
|- ( R e. ( Subcat ` D ) -> D e. Cat ) |
14 |
13
|
adantr |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> D e. Cat ) |
15 |
6 8 12
|
subcss1 |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R C_ ( Base ` D ) ) |
16 |
11 12 14 8 15
|
rescbas |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> dom dom R = ( Base ` ( D |`cat R ) ) ) |
17 |
16
|
feq3d |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> ( f : ( Base ` C ) --> dom dom R <-> f : ( Base ` C ) --> ( Base ` ( D |`cat R ) ) ) ) |
18 |
10 17
|
mpbird |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f : ( Base ` C ) --> dom dom R ) |
19 |
|
eqid |
|- ( Hom ` ( D |`cat R ) ) = ( Hom ` ( D |`cat R ) ) |
20 |
|
simplr |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> f ( C Func ( D |`cat R ) ) g ) |
21 |
|
simprl |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) ) |
22 |
|
simprr |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) ) |
23 |
4 5 19 20 21 22
|
funcf2 |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) ) |
24 |
11 12 14 8 15
|
reschom |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> R = ( Hom ` ( D |`cat R ) ) ) |
25 |
24
|
adantr |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> R = ( Hom ` ( D |`cat R ) ) ) |
26 |
25
|
oveqd |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( f ` x ) R ( f ` y ) ) = ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) ) |
27 |
26
|
feq3d |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) R ( f ` y ) ) <-> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) ( Hom ` ( D |`cat R ) ) ( f ` y ) ) ) ) |
28 |
23 27
|
mpbird |
|- ( ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) R ( f ` y ) ) ) |
29 |
4 5 6 8 18 28
|
funcres2b |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> ( f ( C Func D ) g <-> f ( C Func ( D |`cat R ) ) g ) ) |
30 |
3 29
|
mpbird |
|- ( ( R e. ( Subcat ` D ) /\ f ( C Func ( D |`cat R ) ) g ) -> f ( C Func D ) g ) |
31 |
30
|
ex |
|- ( R e. ( Subcat ` D ) -> ( f ( C Func ( D |`cat R ) ) g -> f ( C Func D ) g ) ) |
32 |
|
df-br |
|- ( f ( C Func ( D |`cat R ) ) g <-> <. f , g >. e. ( C Func ( D |`cat R ) ) ) |
33 |
|
df-br |
|- ( f ( C Func D ) g <-> <. f , g >. e. ( C Func D ) ) |
34 |
31 32 33
|
3imtr3g |
|- ( R e. ( Subcat ` D ) -> ( <. f , g >. e. ( C Func ( D |`cat R ) ) -> <. f , g >. e. ( C Func D ) ) ) |
35 |
2 34
|
relssdv |
|- ( R e. ( Subcat ` D ) -> ( C Func ( D |`cat R ) ) C_ ( C Func D ) ) |