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