Metamath Proof Explorer

Theorem issubc

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 )
issubc.s 
|- ( ph -> S = dom dom J )
Assertion 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 ) ) ) ) )

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 issubc.s 
 |-  ( ph -> S = dom dom J )
6 simpl 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> C e. Cat )
7 sscpwex 
 |-  { j | j C_cat ( Homf ` c ) } e. _V
8 simpl 
 |-  ( ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) -> j C_cat ( Homf ` c ) )
9 8 ss2abi 
 |-  { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } C_ { j | j C_cat ( Homf ` c ) }
10 7 9 ssexi 
 |-  { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } e. _V
11 10 csbex 
 |-  [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } e. _V
12 11 a1i 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } e. _V )
13 df-subc 
 |-  Subcat = ( c e. Cat |-> { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } )
14 13 fvmpts 
 |-  ( ( C e. Cat /\ [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } e. _V ) -> ( Subcat ` C ) = [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } )
15 6 12 14 syl2anc 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> ( Subcat ` C ) = [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } )
16 15 eleq2d 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> ( J e. ( Subcat ` C ) <-> J e. [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } ) )
17 sbcel2 
 |-  ( [. C / c ]. J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> J e. [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } )
18 17 a1i 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> ( [. C / c ]. J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> J e. [_ C / c ]_ { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } ) )
19 elex 
 |-  ( J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } -> J e. _V )
20 19 a1i 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> ( J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } -> J e. _V ) )
21 sscrel 
 |-  Rel C_cat
22 21 brrelex1i 
 |-  ( J C_cat H -> J e. _V )
23 22 adantr 
 |-  ( ( 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 ) ) ) -> J e. _V )
24 23 a1i 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = 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 ) ) ) -> J e. _V ) )
25 df-sbc 
 |-  ( [. J / j ]. ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) <-> J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } )
26 simpr 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ J e. _V ) -> J e. _V )
27 simpr 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> j = J )
28 simpr 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> c = C )
29 28 fveq2d 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> ( Homf ` c ) = ( Homf ` C ) )
30 29 1 eqtr4di 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> ( Homf ` c ) = H )
31 30 adantr 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> ( Homf ` c ) = H )
32 27 31 breq12d 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> ( j C_cat ( Homf ` c ) <-> J C_cat H ) )
33 vex 
 |-  j e. _V
34 33 dmex 
 |-  dom j e. _V
35 34 dmex 
 |-  dom dom j e. _V
36 35 a1i 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> dom dom j e. _V )
37 27 dmeqd 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> dom j = dom J )
38 37 dmeqd 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> dom dom j = dom dom J )
39 simpllr 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> S = dom dom J )
40 38 39 eqtr4d 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> dom dom j = S )
41 simpr 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> s = S )
42 simpllr 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> c = C )
43 42 fveq2d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( Id ` c ) = ( Id ` C ) )
44 43 2 eqtr4di 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( Id ` c ) = .1. )
45 44 fveq1d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( ( Id ` c ) ` x ) = ( .1. ` x ) )
46 simplr 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> j = J )
47 46 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( x j x ) = ( x J x ) )
48 45 47 eleq12d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( ( ( Id ` c ) ` x ) e. ( x j x ) <-> ( .1. ` x ) e. ( x J x ) ) )
49 46 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( x j y ) = ( x J y ) )
50 46 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( y j z ) = ( y J z ) )
51 42 fveq2d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( comp ` c ) = ( comp ` C ) )
52 51 3 eqtr4di 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( comp ` c ) = .x. )
53 52 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( <. x , y >. ( comp ` c ) z ) = ( <. x , y >. .x. z ) )
54 53 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( g ( <. x , y >. ( comp ` c ) z ) f ) = ( g ( <. x , y >. .x. z ) f ) )
55 46 oveqd 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( x j z ) = ( x J z ) )
56 54 55 eleq12d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) <-> ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) )
57 50 56 raleqbidv 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) <-> A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) )
58 49 57 raleqbidv 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = 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. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) ) )
59 41 58 raleqbidv 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = 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. 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 ) ) )
60 41 59 raleqbidv 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = 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 ) <-> 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 ) ) )
61 48 60 anbi12d 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) <-> ( ( .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 ) ) ) )
62 41 61 raleqbidv 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) /\ s = S ) -> ( 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) <-> 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 ) ) ) )
63 36 40 62 sbcied2 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> ( [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) <-> 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 ) ) ) )
64 32 63 anbi12d 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ j = J ) -> ( ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) <-> ( 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 ) ) ) ) )
65 64 adantlr 
 |-  ( ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ J e. _V ) /\ j = J ) -> ( ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) <-> ( 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 ) ) ) ) )
66 26 65 sbcied 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ J e. _V ) -> ( [. J / j ]. ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) <-> ( 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 ) ) ) ) )
67 25 66 bitr3id 
 |-  ( ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) /\ J e. _V ) -> ( J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> ( 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 ) ) ) ) )
68 67 ex 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> ( J e. _V -> ( J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> ( 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 ) ) ) ) ) )
69 20 24 68 pm5.21ndd 
 |-  ( ( ( C e. Cat /\ S = dom dom J ) /\ c = C ) -> ( J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> ( 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 ) ) ) ) )
70 6 69 sbcied 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> ( [. C / c ]. J e. { j | ( j C_cat ( Homf ` c ) /\ [. dom dom j / s ]. 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 >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) } <-> ( 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 ) ) ) ) )
71 16 18 70 3bitr2d 
 |-  ( ( C e. Cat /\ S = dom dom J ) -> ( 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 ) ) ) ) )
72 4 5 71 syl2anc 
 |-  ( 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 ) ) ) ) )