Metamath Proof Explorer


Theorem issubc2

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 ) ) ) ) )

Proof

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 ) ) ) ) )