Step |
Hyp |
Ref |
Expression |
1 |
|
oveq1 |
|- ( c = C -> ( c Faith d ) = ( C Faith d ) ) |
2 |
|
oveq1 |
|- ( c = C -> ( c Func d ) = ( C Func d ) ) |
3 |
1 2
|
sseq12d |
|- ( c = C -> ( ( c Faith d ) C_ ( c Func d ) <-> ( C Faith d ) C_ ( C Func d ) ) ) |
4 |
|
oveq2 |
|- ( d = D -> ( C Faith d ) = ( C Faith D ) ) |
5 |
|
oveq2 |
|- ( d = D -> ( C Func d ) = ( C Func D ) ) |
6 |
4 5
|
sseq12d |
|- ( d = D -> ( ( C Faith d ) C_ ( C Func d ) <-> ( C Faith D ) C_ ( C Func D ) ) ) |
7 |
|
ovex |
|- ( c Func d ) e. _V |
8 |
|
simpl |
|- ( ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) -> f ( c Func d ) g ) |
9 |
8
|
ssopab2i |
|- { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } C_ { <. f , g >. | f ( c Func d ) g } |
10 |
|
opabss |
|- { <. f , g >. | f ( c Func d ) g } C_ ( c Func d ) |
11 |
9 10
|
sstri |
|- { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } C_ ( c Func d ) |
12 |
7 11
|
ssexi |
|- { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } e. _V |
13 |
|
df-fth |
|- Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } ) |
14 |
13
|
ovmpt4g |
|- ( ( c e. Cat /\ d e. Cat /\ { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } e. _V ) -> ( c Faith d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } ) |
15 |
12 14
|
mp3an3 |
|- ( ( c e. Cat /\ d e. Cat ) -> ( c Faith d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } ) |
16 |
15 11
|
eqsstrdi |
|- ( ( c e. Cat /\ d e. Cat ) -> ( c Faith d ) C_ ( c Func d ) ) |
17 |
3 6 16
|
vtocl2ga |
|- ( ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) C_ ( C Func D ) ) |
18 |
13
|
mpondm0 |
|- ( -. ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) = (/) ) |
19 |
|
0ss |
|- (/) C_ ( C Func D ) |
20 |
18 19
|
eqsstrdi |
|- ( -. ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) C_ ( C Func D ) ) |
21 |
17 20
|
pm2.61i |
|- ( C Faith D ) C_ ( C Func D ) |