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

Proof

Step Hyp Ref Expression
1 iinfsubc.1 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
2 iinfsubc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
3 iinfsubc.3 ⊢ ( 𝜑 → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
4 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5 2 4 subcssc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat ( Homf ‘ 𝐶 ) )
6 1 5 3 iinfssc ⊢ ( 𝜑 → 𝐾 ⊆cat ( Homf ‘ 𝐶 ) )
7 2 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑎 ∈ dom dom 𝐻 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐻 = dom dom 𝐻 )
9 2 8 subcfn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
10 9 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑎 ∈ dom dom 𝐻 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
11 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑎 ∈ dom dom 𝐻 ) → 𝑎 ∈ dom dom 𝐻 )
12 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
13 7 10 11 12 subcidcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑎 ∈ dom dom 𝐻 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) )
14 13 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑎 ∈ dom dom 𝐻 → ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) ) )
15 14 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 → ∀ 𝑥 ∈ 𝐴 ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) ) )
16 eliin ⊢ ( 𝑎 ∈ V → ( 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀ 𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 ) )
17 16 elv ⊢ ( 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ↔ ∀ 𝑥 ∈ 𝐴 𝑎 ∈ dom dom 𝐻 )
18 fvex ⊢ ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ V
19 eliin ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ V → ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑎 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) ) )
20 18 19 ax-mp ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑎 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐻 𝑎 ) )
21 15 17 20 3imtr4g ⊢ ( 𝜑 → ( 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 → ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑎 ) ) )
22 21 imp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑎 ) )
23 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → 𝐴 ≠ ∅ )
24 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat ( Homf ‘ 𝐶 ) )
25 3 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
26 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐻 = dom dom 𝐻 )
27 nfv ⊢ Ⅎ 𝑥 𝜑
28 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
29 28 nfcri ⊢ Ⅎ 𝑥 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
30 27 29 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
32 23 24 25 26 30 31 31 iinfssclem3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → ( 𝑎 𝐾 𝑎 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑎 ) )
33 22 32 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) )
34 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) )
35 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝐴 ≠ ∅ )
36 24 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ⊆cat ( Homf ‘ 𝐶 ) )
37 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝐾 = ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 dom 𝐻 ↦ ∩ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) ) )
38 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ 𝑥 ∈ 𝐴 ) → dom dom 𝐻 = dom dom 𝐻 )
39 28 nfcri ⊢ Ⅎ 𝑥 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
40 28 nfcri ⊢ Ⅎ 𝑥 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻
41 39 40 nfan ⊢ Ⅎ 𝑥 ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
42 30 41 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) )
43 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
44 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
45 35 36 37 38 42 43 44 iinfssclem3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝑎 𝐾 𝑏 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) )
46 45 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑎 𝐾 𝑏 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) )
47 34 46 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) )
48 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) )
49 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
50 35 36 37 38 42 44 49 iinfssclem3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝑏 𝐾 𝑐 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) )
51 50 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑏 𝐾 𝑐 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) )
52 48 51 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) )
53 47 52 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) )
54 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 )
55 54 nfcri ⊢ Ⅎ 𝑥 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 )
56 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 )
57 56 nfcri ⊢ Ⅎ 𝑥 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 )
58 55 57 nfan ⊢ Ⅎ 𝑥 ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) )
59 42 58 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) )
60 2 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 ∈ ( Subcat ‘ 𝐶 ) )
61 9 ad5ant15 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐻 Fn ( dom dom 𝐻 × dom dom 𝐻 ) )
62 iinss2 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻 )
63 62 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ⊆ dom dom 𝐻 )
64 43 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
65 63 64 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑎 ∈ dom dom 𝐻 )
66 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
67 44 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
68 63 67 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑏 ∈ dom dom 𝐻 )
69 49 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 )
70 63 69 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑐 ∈ dom dom 𝐻 )
71 iinss2 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ⊆ ( 𝑎 𝐻 𝑏 ) )
72 71 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ⊆ ( 𝑎 𝐻 𝑏 ) )
73 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) )
74 72 73 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) )
75 iinss2 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ⊆ ( 𝑏 𝐻 𝑐 ) )
76 75 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ⊆ ( 𝑏 𝐻 𝑐 ) )
77 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) )
78 76 77 sseldd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) )
79 60 61 65 66 68 70 74 78 subccocl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐻 𝑐 ) )
80 59 79 ralrimia ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐻 𝑐 ) )
81 ovex ⊢ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ V
82 eliin ⊢ ( ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ V → ( ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐻 𝑐 ) ) )
83 81 82 ax-mp ⊢ ( ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐻 𝑐 ) )
84 80 83 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑏 ) ∧ 𝑔 ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑏 𝐻 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) )
85 53 84 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) )
86 35 36 37 38 42 43 49 iinfssclem3 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ( 𝑎 𝐾 𝑐 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) )
87 86 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑎 𝐾 𝑐 ) = ∩ 𝑥 ∈ 𝐴 ( 𝑎 𝐻 𝑐 ) )
88 85 87 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) ∧ ( 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∧ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ) ) → ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
89 88 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ∧ ( 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∧ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) ) → ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
90 89 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → ∀ 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) )
91 33 90 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) )
92 91 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) )
93 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
94 1 93 sylib ⊢ ( 𝜑 → ∃ 𝑥 𝑥 ∈ 𝐴 )
95 subcrcl ⊢ ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
96 2 95 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ Cat )
97 94 96 exlimddv ⊢ ( 𝜑 → 𝐶 ∈ Cat )
98 1 5 3 8 27 iinfssclem2 ⊢ ( 𝜑 → 𝐾 Fn ( ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 × ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ) )
99 4 12 66 97 98 issubc2 ⊢ ( 𝜑 → ( 𝐾 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐾 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑎 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ( ( ( Id ‘ 𝐶 ) ‘ 𝑎 ) ∈ ( 𝑎 𝐾 𝑎 ) ∧ ∀ 𝑏 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑐 ∈ ∩ 𝑥 ∈ 𝐴 dom dom 𝐻 ∀ 𝑓 ∈ ( 𝑎 𝐾 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐾 𝑐 ) ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐶 ) 𝑐 ) 𝑓 ) ∈ ( 𝑎 𝐾 𝑐 ) ) ) ) )
100 6 92 99 mpbir2and ⊢ ( 𝜑 → 𝐾 ∈ ( Subcat ‘ 𝐶 ) )