Metamath Proof Explorer

Theorem iinfsubc

Description: Indexed intersection of subcategories is a subcategory. (Contributed by Zhi Wang, 31-Oct-2025)

Ref Expression
Hypotheses iinfsubc.1 
|- ( ph -> A =/= (/) )
iinfsubc.2 
|- ( ( ph /\ x e. A ) -> H e. ( Subcat ` C ) )
iinfsubc.3 
|- ( ph -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
Assertion iinfsubc 
|- ( ph -> K e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 iinfsubc.1 
 |-  ( ph -> A =/= (/) )
2 iinfsubc.2 
 |-  ( ( ph /\ x e. A ) -> H e. ( Subcat ` C ) )
3 iinfsubc.3 
 |-  ( ph -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
4 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
5 2 4 subcssc 
 |-  ( ( ph /\ x e. A ) -> H C_cat ( Homf ` C ) )
6 1 5 3 iinfssc 
 |-  ( ph -> K C_cat ( Homf ` C ) )
7 2 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ a e. dom dom H ) -> H e. ( Subcat ` C ) )
8 eqidd 
 |-  ( ( ph /\ x e. A ) -> dom dom H = dom dom H )
9 2 8 subcfn 
 |-  ( ( ph /\ x e. A ) -> H Fn ( dom dom H X. dom dom H ) )
10 9 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ a e. dom dom H ) -> H Fn ( dom dom H X. dom dom H ) )
11 simpr 
 |-  ( ( ( ph /\ x e. A ) /\ a e. dom dom H ) -> a e. dom dom H )
12 eqid 
 |-  ( Id ` C ) = ( Id ` C )
13 7 10 11 12 subcidcl 
 |-  ( ( ( ph /\ x e. A ) /\ a e. dom dom H ) -> ( ( Id ` C ) ` a ) e. ( a H a ) )
14 13 ex 
 |-  ( ( ph /\ x e. A ) -> ( a e. dom dom H -> ( ( Id ` C ) ` a ) e. ( a H a ) ) )
15 14 ralimdva 
 |-  ( ph -> ( A. x e. A a e. dom dom H -> A. x e. A ( ( Id ` C ) ` a ) e. ( a H a ) ) )
16 eliin 
 |-  ( a e. _V -> ( a e. |^|_ x e. A dom dom H <-> A. x e. A a e. dom dom H ) )
17 16 elv 
 |-  ( a e. |^|_ x e. A dom dom H <-> A. x e. A a e. dom dom H )
18 fvex 
 |-  ( ( Id ` C ) ` a ) e. _V
19 eliin 
 |-  ( ( ( Id ` C ) ` a ) e. _V -> ( ( ( Id ` C ) ` a ) e. |^|_ x e. A ( a H a ) <-> A. x e. A ( ( Id ` C ) ` a ) e. ( a H a ) ) )
20 18 19 ax-mp 
 |-  ( ( ( Id ` C ) ` a ) e. |^|_ x e. A ( a H a ) <-> A. x e. A ( ( Id ` C ) ` a ) e. ( a H a ) )
21 15 17 20 3imtr4g 
 |-  ( ph -> ( a e. |^|_ x e. A dom dom H -> ( ( Id ` C ) ` a ) e. |^|_ x e. A ( a H a ) ) )
22 21 imp 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> ( ( Id ` C ) ` a ) e. |^|_ x e. A ( a H a ) )
23 1 adantr 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> A =/= (/) )
24 5 adantlr 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ x e. A ) -> H C_cat ( Homf ` C ) )
25 3 adantr 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
26 eqidd 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ x e. A ) -> dom dom H = dom dom H )
27 nfv 
 |-  F/ x ph
28 nfii1 
 |-  F/_ x |^|_ x e. A dom dom H
29 28 nfcri 
 |-  F/ x a e. |^|_ x e. A dom dom H
30 27 29 nfan 
 |-  F/ x ( ph /\ a e. |^|_ x e. A dom dom H )
31 simpr 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> a e. |^|_ x e. A dom dom H )
32 23 24 25 26 30 31 31 iinfssclem3 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> ( a K a ) = |^|_ x e. A ( a H a ) )
33 22 32 eleqtrrd 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> ( ( Id ` C ) ` a ) e. ( a K a ) )
34 simprl 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> f e. ( a K b ) )
35 1 ad2antrr 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> A =/= (/) )
36 24 adantlr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> H C_cat ( Homf ` C ) )
37 3 ad2antrr 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
38 eqidd 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> dom dom H = dom dom H )
39 28 nfcri 
 |-  F/ x b e. |^|_ x e. A dom dom H
40 28 nfcri 
 |-  F/ x c e. |^|_ x e. A dom dom H
41 39 40 nfan 
 |-  F/ x ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H )
42 30 41 nfan 
 |-  F/ x ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) )
43 31 adantr 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> a e. |^|_ x e. A dom dom H )
44 simprl 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> b e. |^|_ x e. A dom dom H )
45 35 36 37 38 42 43 44 iinfssclem3 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> ( a K b ) = |^|_ x e. A ( a H b ) )
46 45 adantr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( a K b ) = |^|_ x e. A ( a H b ) )
47 34 46 eleqtrd 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> f e. |^|_ x e. A ( a H b ) )
48 simprr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> g e. ( b K c ) )
49 simprr 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> c e. |^|_ x e. A dom dom H )
50 35 36 37 38 42 44 49 iinfssclem3 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> ( b K c ) = |^|_ x e. A ( b H c ) )
51 50 adantr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( b K c ) = |^|_ x e. A ( b H c ) )
52 48 51 eleqtrd 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> g e. |^|_ x e. A ( b H c ) )
53 47 52 jca 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) )
54 nfii1 
 |-  F/_ x |^|_ x e. A ( a H b )
55 54 nfcri 
 |-  F/ x f e. |^|_ x e. A ( a H b )
56 nfii1 
 |-  F/_ x |^|_ x e. A ( b H c )
57 56 nfcri 
 |-  F/ x g e. |^|_ x e. A ( b H c )
58 55 57 nfan 
 |-  F/ x ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) )
59 42 58 nfan 
 |-  F/ x ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) )
60 2 ad5ant15 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> H e. ( Subcat ` C ) )
61 9 ad5ant15 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> H Fn ( dom dom H X. dom dom H ) )
62 iinss2 
 |-  ( x e. A -> |^|_ x e. A dom dom H C_ dom dom H )
63 62 adantl 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> |^|_ x e. A dom dom H C_ dom dom H )
64 43 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> a e. |^|_ x e. A dom dom H )
65 63 64 sseldd 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> a e. dom dom H )
66 eqid 
 |-  ( comp ` C ) = ( comp ` C )
67 44 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> b e. |^|_ x e. A dom dom H )
68 63 67 sseldd 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> b e. dom dom H )
69 49 ad2antrr 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> c e. |^|_ x e. A dom dom H )
70 63 69 sseldd 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> c e. dom dom H )
71 iinss2 
 |-  ( x e. A -> |^|_ x e. A ( a H b ) C_ ( a H b ) )
72 71 adantl 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> |^|_ x e. A ( a H b ) C_ ( a H b ) )
73 simplrl 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> f e. |^|_ x e. A ( a H b ) )
74 72 73 sseldd 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> f e. ( a H b ) )
75 iinss2 
 |-  ( x e. A -> |^|_ x e. A ( b H c ) C_ ( b H c ) )
76 75 adantl 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> |^|_ x e. A ( b H c ) C_ ( b H c ) )
77 simplrr 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> g e. |^|_ x e. A ( b H c ) )
78 76 77 sseldd 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> g e. ( b H c ) )
79 60 61 65 66 68 70 74 78 subccocl 
 |-  ( ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) /\ x e. A ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a H c ) )
80 59 79 ralrimia 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) -> A. x e. A ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a H c ) )
81 ovex 
 |-  ( g ( <. a , b >. ( comp ` C ) c ) f ) e. _V
82 eliin 
 |-  ( ( g ( <. a , b >. ( comp ` C ) c ) f ) e. _V -> ( ( g ( <. a , b >. ( comp ` C ) c ) f ) e. |^|_ x e. A ( a H c ) <-> A. x e. A ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a H c ) ) )
83 81 82 ax-mp 
 |-  ( ( g ( <. a , b >. ( comp ` C ) c ) f ) e. |^|_ x e. A ( a H c ) <-> A. x e. A ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a H c ) )
84 80 83 sylibr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. |^|_ x e. A ( a H b ) /\ g e. |^|_ x e. A ( b H c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) e. |^|_ x e. A ( a H c ) )
85 53 84 syldan 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) e. |^|_ x e. A ( a H c ) )
86 35 36 37 38 42 43 49 iinfssclem3 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> ( a K c ) = |^|_ x e. A ( a H c ) )
87 86 adantr 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( a K c ) = |^|_ x e. A ( a H c ) )
88 85 87 eleqtrrd 
 |-  ( ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) /\ ( f e. ( a K b ) /\ g e. ( b K c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) )
89 88 ralrimivva 
 |-  ( ( ( ph /\ a e. |^|_ x e. A dom dom H ) /\ ( b e. |^|_ x e. A dom dom H /\ c e. |^|_ x e. A dom dom H ) ) -> A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) )
90 89 ralrimivva 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> A. b e. |^|_ x e. A dom dom H A. c e. |^|_ x e. A dom dom H A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) )
91 33 90 jca 
 |-  ( ( ph /\ a e. |^|_ x e. A dom dom H ) -> ( ( ( Id ` C ) ` a ) e. ( a K a ) /\ A. b e. |^|_ x e. A dom dom H A. c e. |^|_ x e. A dom dom H A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) ) )
92 91 ralrimiva 
 |-  ( ph -> A. a e. |^|_ x e. A dom dom H ( ( ( Id ` C ) ` a ) e. ( a K a ) /\ A. b e. |^|_ x e. A dom dom H A. c e. |^|_ x e. A dom dom H A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) ) )
93 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
94 1 93 sylib 
 |-  ( ph -> E. x x e. A )
95 subcrcl 
 |-  ( H e. ( Subcat ` C ) -> C e. Cat )
96 2 95 syl 
 |-  ( ( ph /\ x e. A ) -> C e. Cat )
97 94 96 exlimddv 
 |-  ( ph -> C e. Cat )
98 1 5 3 8 27 iinfssclem2 
 |-  ( ph -> K Fn ( |^|_ x e. A dom dom H X. |^|_ x e. A dom dom H ) )
99 4 12 66 97 98 issubc2 
 |-  ( ph -> ( K e. ( Subcat ` C ) <-> ( K C_cat ( Homf ` C ) /\ A. a e. |^|_ x e. A dom dom H ( ( ( Id ` C ) ` a ) e. ( a K a ) /\ A. b e. |^|_ x e. A dom dom H A. c e. |^|_ x e. A dom dom H A. f e. ( a K b ) A. g e. ( b K c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a K c ) ) ) ) )
100 6 92 99 mpbir2and 
 |-  ( ph -> K e. ( Subcat ` C ) )