Step |
Hyp |
Ref |
Expression |
1 |
|
issubc3.h |
|- H = ( Homf ` C ) |
2 |
|
issubc3.i |
|- .1. = ( Id ` C ) |
3 |
|
issubc3.1 |
|- D = ( C |`cat J ) |
4 |
|
issubc3.c |
|- ( ph -> C e. Cat ) |
5 |
|
issubc3.a |
|- ( ph -> J Fn ( S X. S ) ) |
6 |
|
simpr |
|- ( ( ph /\ J e. ( Subcat ` C ) ) -> J e. ( Subcat ` C ) ) |
7 |
6 1
|
subcssc |
|- ( ( ph /\ J e. ( Subcat ` C ) ) -> J C_cat H ) |
8 |
6
|
adantr |
|- ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> J e. ( Subcat ` C ) ) |
9 |
5
|
ad2antrr |
|- ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> J Fn ( S X. S ) ) |
10 |
|
simpr |
|- ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> x e. S ) |
11 |
8 9 10 2
|
subcidcl |
|- ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> ( .1. ` x ) e. ( x J x ) ) |
12 |
11
|
ralrimiva |
|- ( ( ph /\ J e. ( Subcat ` C ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) ) |
13 |
3 6
|
subccat |
|- ( ( ph /\ J e. ( Subcat ` C ) ) -> D e. Cat ) |
14 |
7 12 13
|
3jca |
|- ( ( ph /\ J e. ( Subcat ` C ) ) -> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) |
15 |
|
simpr1 |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J C_cat H ) |
16 |
|
simpr2 |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) ) |
17 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
18 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
19 |
|
eqid |
|- ( comp ` D ) = ( comp ` D ) |
20 |
|
simplrr |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> D e. Cat ) |
21 |
|
simprl1 |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> x e. S ) |
22 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
23 |
4
|
ad2antrr |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> C e. Cat ) |
24 |
5
|
ad2antrr |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J Fn ( S X. S ) ) |
25 |
1 22
|
homffn |
|- H Fn ( ( Base ` C ) X. ( Base ` C ) ) |
26 |
25
|
a1i |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) ) |
27 |
|
simplrl |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J C_cat H ) |
28 |
24 26 27
|
ssc1 |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> S C_ ( Base ` C ) ) |
29 |
3 22 23 24 28
|
rescbas |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> S = ( Base ` D ) ) |
30 |
21 29
|
eleqtrd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> x e. ( Base ` D ) ) |
31 |
|
simprl2 |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> y e. S ) |
32 |
31 29
|
eleqtrd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> y e. ( Base ` D ) ) |
33 |
|
simprl3 |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> z e. S ) |
34 |
33 29
|
eleqtrd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> z e. ( Base ` D ) ) |
35 |
|
simprrl |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> f e. ( x J y ) ) |
36 |
3 22 23 24 28
|
reschom |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J = ( Hom ` D ) ) |
37 |
36
|
oveqd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( x J y ) = ( x ( Hom ` D ) y ) ) |
38 |
35 37
|
eleqtrd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> f e. ( x ( Hom ` D ) y ) ) |
39 |
|
simprrr |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> g e. ( y J z ) ) |
40 |
36
|
oveqd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( y J z ) = ( y ( Hom ` D ) z ) ) |
41 |
39 40
|
eleqtrd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> g e. ( y ( Hom ` D ) z ) ) |
42 |
17 18 19 20 30 32 34 38 41
|
catcocl |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) ) |
43 |
|
eqid |
|- ( comp ` C ) = ( comp ` C ) |
44 |
3 22 23 24 28 43
|
rescco |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( comp ` C ) = ( comp ` D ) ) |
45 |
44
|
oveqd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` D ) z ) ) |
46 |
45
|
oveqd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) ) |
47 |
36
|
oveqd |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( x J z ) = ( x ( Hom ` D ) z ) ) |
48 |
42 46 47
|
3eltr4d |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) |
49 |
48
|
anassrs |
|- ( ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) |
50 |
49
|
ralrimivva |
|- ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) |
51 |
50
|
ralrimivvva |
|- ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) |
52 |
51
|
3adantr2 |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) |
53 |
|
r19.26 |
|- ( A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) <-> ( A. x e. S ( .1. ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) |
54 |
16 52 53
|
sylanbrc |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) |
55 |
4
|
adantr |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> C e. Cat ) |
56 |
5
|
adantr |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J Fn ( S X. S ) ) |
57 |
1 2 43 55 56
|
issubc2 |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) ) |
58 |
15 54 57
|
mpbir2and |
|- ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J e. ( Subcat ` C ) ) |
59 |
14 58
|
impbida |
|- ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) ) |