Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | issubc.h | |- H = ( Homf ` C ) |
|
issubc.i | |- .1. = ( Id ` C ) |
||
issubc.o | |- .x. = ( comp ` C ) |
||
issubc.c | |- ( ph -> C e. Cat ) |
||
issubc2.a | |- ( ph -> J Fn ( S X. S ) ) |
||
Assertion | issubc2 | |- ( ph -> ( 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 >. .x. z ) f ) e. ( x J z ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issubc.h | |- H = ( Homf ` C ) |
|
2 | issubc.i | |- .1. = ( Id ` C ) |
|
3 | issubc.o | |- .x. = ( comp ` C ) |
|
4 | issubc.c | |- ( ph -> C e. Cat ) |
|
5 | issubc2.a | |- ( ph -> J Fn ( S X. S ) ) |
|
6 | 5 | fndmd | |- ( ph -> dom J = ( S X. S ) ) |
7 | 6 | dmeqd | |- ( ph -> dom dom J = dom ( S X. S ) ) |
8 | dmxpid | |- dom ( S X. S ) = S |
|
9 | 7 8 | eqtr2di | |- ( ph -> S = dom dom J ) |
10 | 1 2 3 4 9 | issubc | |- ( ph -> ( 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 >. .x. z ) f ) e. ( x J z ) ) ) ) ) |