Step |
Hyp |
Ref |
Expression |
1 |
|
subcidcl.j |
|- ( ph -> J e. ( Subcat ` C ) ) |
2 |
|
subcidcl.2 |
|- ( ph -> J Fn ( S X. S ) ) |
3 |
|
subcidcl.x |
|- ( ph -> X e. S ) |
4 |
|
subccocl.o |
|- .x. = ( comp ` C ) |
5 |
|
subccocl.y |
|- ( ph -> Y e. S ) |
6 |
|
subccocl.z |
|- ( ph -> Z e. S ) |
7 |
|
subccocl.f |
|- ( ph -> F e. ( X J Y ) ) |
8 |
|
subccocl.g |
|- ( ph -> G e. ( Y J Z ) ) |
9 |
|
eqid |
|- ( Homf ` C ) = ( Homf ` C ) |
10 |
|
eqid |
|- ( Id ` C ) = ( Id ` C ) |
11 |
|
subcrcl |
|- ( J e. ( Subcat ` C ) -> C e. Cat ) |
12 |
1 11
|
syl |
|- ( ph -> C e. Cat ) |
13 |
9 10 4 12 2
|
issubc2 |
|- ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( ( Id ` C ) ` 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 >. .x. z ) f ) e. ( x J z ) ) ) ) ) |
14 |
1 13
|
mpbid |
|- ( ph -> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( ( Id ` C ) ` 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 >. .x. z ) f ) e. ( x J z ) ) ) ) |
15 |
14
|
simprd |
|- ( ph -> A. x e. S ( ( ( Id ` C ) ` 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 >. .x. z ) f ) e. ( x J z ) ) ) |
16 |
5
|
adantr |
|- ( ( ph /\ x = X ) -> Y e. S ) |
17 |
6
|
ad2antrr |
|- ( ( ( ph /\ x = X ) /\ y = Y ) -> Z e. S ) |
18 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( X J Y ) ) |
19 |
|
simpllr |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> x = X ) |
20 |
|
simplr |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> y = Y ) |
21 |
19 20
|
oveq12d |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( x J y ) = ( X J Y ) ) |
22 |
18 21
|
eleqtrrd |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> F e. ( x J y ) ) |
23 |
8
|
ad4antr |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( Y J Z ) ) |
24 |
|
simpllr |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> y = Y ) |
25 |
|
simplr |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> z = Z ) |
26 |
24 25
|
oveq12d |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( y J z ) = ( Y J Z ) ) |
27 |
23 26
|
eleqtrrd |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> G e. ( y J z ) ) |
28 |
|
simp-5r |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> x = X ) |
29 |
|
simp-4r |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> y = Y ) |
30 |
28 29
|
opeq12d |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> <. x , y >. = <. X , Y >. ) |
31 |
|
simpllr |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> z = Z ) |
32 |
30 31
|
oveq12d |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( <. x , y >. .x. z ) = ( <. X , Y >. .x. Z ) ) |
33 |
|
simpr |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> g = G ) |
34 |
|
simplr |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> f = F ) |
35 |
32 33 34
|
oveq123d |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( g ( <. x , y >. .x. z ) f ) = ( G ( <. X , Y >. .x. Z ) F ) ) |
36 |
28 31
|
oveq12d |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( x J z ) = ( X J Z ) ) |
37 |
35 36
|
eleq12d |
|- ( ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) /\ g = G ) -> ( ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) <-> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
38 |
27 37
|
rspcdv |
|- ( ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) /\ f = F ) -> ( A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
39 |
22 38
|
rspcimdv |
|- ( ( ( ( ph /\ x = X ) /\ y = Y ) /\ z = Z ) -> ( A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
40 |
17 39
|
rspcimdv |
|- ( ( ( ph /\ x = X ) /\ y = Y ) -> ( A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
41 |
16 40
|
rspcimdv |
|- ( ( ph /\ x = X ) -> ( A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
42 |
41
|
adantld |
|- ( ( ph /\ x = X ) -> ( ( ( ( Id ` C ) ` 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 >. .x. z ) f ) e. ( x J z ) ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
43 |
3 42
|
rspcimdv |
|- ( ph -> ( A. x e. S ( ( ( Id ` C ) ` 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 >. .x. z ) f ) e. ( x J z ) ) -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) ) |
44 |
15 43
|
mpd |
|- ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. ( X J Z ) ) |