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 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
iinfssc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat 𝐽 )
iinfssc.3 ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
Assertion iinfssc ( 𝜑 → 𝐾 ⊆cat 𝐽 )

Proof

Step Hyp Ref Expression
1 iinfssc.1 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2 iinfssc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat 𝐽 )
3 iinfssc.3 ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
4 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐻 = dom dom 𝐻 )
5 2 4 sscfn1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
6 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐽 = dom dom 𝐽 )
7 2 6 sscfn2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
8 5 7 2 ssc1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐻 ⊆ dom dom 𝐽 )
9 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 )
10 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 ) → ∃ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 )
11 1 9 10 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 )
12 iinss ⊢ ( ∃ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 )
13 11 12 syl ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 )
14 nfv ⊢ Ⅎ 𝑥 𝜑
15 1 2 3 4 14 iinfssclem1 ⊢ ( 𝜑 → 𝐾 = ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 , 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ) )
16 ovex ⊢ ( 𝑧 𝐻 𝑤 ) ∈ V
17 16 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ∈ V
18 iinexg ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ∈ V ) → ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ∈ V )
19 1 17 18 sylancl ⊢ ( 𝜑 → ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ∈ V )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ∈ V )
21 15 20 ovmpt4d ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝑧 𝐾 𝑤 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) )
22 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝐴 ≠ ∅ )
23 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
24 23 nfcri ⊢ Ⅎ 𝑥 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
25 23 nfcri ⊢ Ⅎ 𝑥 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
26 24 25 nfan ⊢ Ⅎ 𝑥 ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
27 14 26 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) )
28 5 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
29 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat 𝐽 )
30 iinss2 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻 )
31 30 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻 )
32 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
33 31 32 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑧 ∈ dom dom 𝐻 )
34 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
35 31 34 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑤 ∈ dom dom 𝐻 )
36 28 29 33 35 ssc2 ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
37 27 36 ralrimia ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
38 22 37 jca ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) ) )
39 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
40 iinss ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) → ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
41 38 39 40 3syl ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ∩ 𝑥 ∈ 𝐴 ( 𝑧 𝐻 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
42 21 41 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
43 42 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) )
44 1 2 3 4 14 iinfssclem2 ⊢ ( 𝜑 → 𝐾 Fn ( ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) )
45 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
46 1 45 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
47 46 7 exlimddv ⊢ ( 𝜑 → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
48 sscrel ⊢ Rel ⊆cat
49 48 brrelex2i ⊢ ( 𝐻 ⊆cat 𝐽 → 𝐽 ∈ V )
50 2 49 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐽 ∈ V )
51 46 50 exlimddv ⊢ ( 𝜑 → 𝐽 ∈ V )
52 51 dmexd ⊢ ( 𝜑 → dom 𝐽 ∈ V )
53 52 dmexd ⊢ ( 𝜑 → dom dom 𝐽 ∈ V )
54 44 47 53 isssc ⊢ ( 𝜑 → ( 𝐾 ⊆cat 𝐽 ↔ ( ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐽 ∧ ∀ 𝑧 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑤 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ( 𝑧 𝐾 𝑤 ) ⊆ ( 𝑧 𝐽 𝑤 ) ) ) )
55 13 43 54 mpbir2and ⊢ ( 𝜑 → 𝐾 ⊆cat 𝐽 )