Metamath Proof Explorer

Theorem iinfssc

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

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

Proof

Step Hyp Ref Expression
1 iinfssc.1 
 |-  ( ph -> A =/= (/) )
2 iinfssc.2 
 |-  ( ( ph /\ x e. A ) -> H C_cat J )
3 iinfssc.3 
 |-  ( ph -> K = ( y e. |^|_ x e. A dom H |-> |^|_ x e. A ( H ` y ) ) )
4 eqidd 
 |-  ( ( ph /\ x e. A ) -> dom dom H = dom dom H )
5 2 4 sscfn1 
 |-  ( ( ph /\ x e. A ) -> H Fn ( dom dom H X. dom dom H ) )
6 eqidd 
 |-  ( ( ph /\ x e. A ) -> dom dom J = dom dom J )
7 2 6 sscfn2 
 |-  ( ( ph /\ x e. A ) -> J Fn ( dom dom J X. dom dom J ) )
8 5 7 2 ssc1 
 |-  ( ( ph /\ x e. A ) -> dom dom H C_ dom dom J )
9 8 ralrimiva 
 |-  ( ph -> A. x e. A dom dom H C_ dom dom J )
10 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A dom dom H C_ dom dom J ) -> E. x e. A dom dom H C_ dom dom J )
11 1 9 10 syl2anc 
 |-  ( ph -> E. x e. A dom dom H C_ dom dom J )
12 iinss 
 |-  ( E. x e. A dom dom H C_ dom dom J -> |^|_ x e. A dom dom H C_ dom dom J )
13 11 12 syl 
 |-  ( ph -> |^|_ x e. A dom dom H C_ dom dom J )
14 nfv 
 |-  F/ x ph
15 1 2 3 4 14 iinfssclem1 
 |-  ( ph -> K = ( z e. |^|_ x e. A dom dom H , w e. |^|_ x e. A dom dom H |-> |^|_ x e. A ( z H w ) ) )
16 ovex 
 |-  ( z H w ) e. _V
17 16 rgenw 
 |-  A. x e. A ( z H w ) e. _V
18 iinexg 
 |-  ( ( A =/= (/) /\ A. x e. A ( z H w ) e. _V ) -> |^|_ x e. A ( z H w ) e. _V )
19 1 17 18 sylancl 
 |-  ( ph -> |^|_ x e. A ( z H w ) e. _V )
20 19 adantr 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> |^|_ x e. A ( z H w ) e. _V )
21 15 20 ovmpt4d 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> ( z K w ) = |^|_ x e. A ( z H w ) )
22 1 adantr 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> A =/= (/) )
23 nfii1 
 |-  F/_ x |^|_ x e. A dom dom H
24 23 nfcri 
 |-  F/ x z e. |^|_ x e. A dom dom H
25 23 nfcri 
 |-  F/ x w e. |^|_ x e. A dom dom H
26 24 25 nfan 
 |-  F/ x ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H )
27 14 26 nfan 
 |-  F/ x ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) )
28 5 adantlr 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> H Fn ( dom dom H X. dom dom H ) )
29 2 adantlr 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> H C_cat J )
30 iinss2 
 |-  ( x e. A -> |^|_ x e. A dom dom H C_ dom dom H )
31 30 adantl 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> |^|_ x e. A dom dom H C_ dom dom H )
32 simplrl 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> z e. |^|_ x e. A dom dom H )
33 31 32 sseldd 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> z e. dom dom H )
34 simplrr 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> w e. |^|_ x e. A dom dom H )
35 31 34 sseldd 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> w e. dom dom H )
36 28 29 33 35 ssc2 
 |-  ( ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) /\ x e. A ) -> ( z H w ) C_ ( z J w ) )
37 27 36 ralrimia 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> A. x e. A ( z H w ) C_ ( z J w ) )
38 22 37 jca 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> ( A =/= (/) /\ A. x e. A ( z H w ) C_ ( z J w ) ) )
39 r19.2z 
 |-  ( ( A =/= (/) /\ A. x e. A ( z H w ) C_ ( z J w ) ) -> E. x e. A ( z H w ) C_ ( z J w ) )
40 iinss 
 |-  ( E. x e. A ( z H w ) C_ ( z J w ) -> |^|_ x e. A ( z H w ) C_ ( z J w ) )
41 38 39 40 3syl 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> |^|_ x e. A ( z H w ) C_ ( z J w ) )
42 21 41 eqsstrd 
 |-  ( ( ph /\ ( z e. |^|_ x e. A dom dom H /\ w e. |^|_ x e. A dom dom H ) ) -> ( z K w ) C_ ( z J w ) )
43 42 ralrimivva 
 |-  ( ph -> A. z e. |^|_ x e. A dom dom H A. w e. |^|_ x e. A dom dom H ( z K w ) C_ ( z J w ) )
44 1 2 3 4 14 iinfssclem2 
 |-  ( ph -> K Fn ( |^|_ x e. A dom dom H X. |^|_ x e. A dom dom H ) )
45 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
46 1 45 sylib 
 |-  ( ph -> E. x x e. A )
47 46 7 exlimddv 
 |-  ( ph -> J Fn ( dom dom J X. dom dom J ) )
48 sscrel 
 |-  Rel C_cat
49 48 brrelex2i 
 |-  ( H C_cat J -> J e. _V )
50 2 49 syl 
 |-  ( ( ph /\ x e. A ) -> J e. _V )
51 46 50 exlimddv 
 |-  ( ph -> J e. _V )
52 51 dmexd 
 |-  ( ph -> dom J e. _V )
53 52 dmexd 
 |-  ( ph -> dom dom J e. _V )
54 44 47 53 isssc 
 |-  ( ph -> ( K C_cat J <-> ( |^|_ x e. A dom dom H C_ dom dom J /\ A. z e. |^|_ x e. A dom dom H A. w e. |^|_ x e. A dom dom H ( z K w ) C_ ( z J w ) ) ) )
55 13 43 54 mpbir2and 
 |-  ( ph -> K C_cat J )