Metamath Proof Explorer

Theorem ssccatid

Description: A category C restricted by J is a category if all of the following are satisfied: a) the base is a subset of base of C , b) all hom-sets are subsets of hom-sets of C , c) it has identity morphisms for all objects, d) the composition under C is closed in J . But J might not be a subcategory of C (see cnelsubc ). (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses ssccatid.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
ssccatid.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
ssccatid.x ⊢ · = ( comp ‘ 𝐶 )
ssccatid.j ⊢ ( 𝜑 → 𝐽 ⊆cat 𝐻 )
ssccatid.f ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
ssccatid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
ssccatid.i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 1 ∈ ( 𝑦 𝐽 𝑦 ) )
ssccatid.l ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 )
ssccatid.r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ) ) → ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 )
ssccatid.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
Assertion ssccatid ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑦 ∈ 𝑆 ↦ 1 ) ) )

Proof

Step Hyp Ref Expression
1 ssccatid.h ⊢ 𝐻 = ( Homf ‘ 𝐶 )
2 ssccatid.d ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
3 ssccatid.x ⊢ · = ( comp ‘ 𝐶 )
4 ssccatid.j ⊢ ( 𝜑 → 𝐽 ⊆cat 𝐻 )
5 ssccatid.f ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
6 ssccatid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
7 ssccatid.i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 1 ∈ ( 𝑦 𝐽 𝑦 ) )
8 ssccatid.l ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ) ) → ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 )
9 ssccatid.r ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ∧ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ) ) → ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 )
10 ssccatid.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 1 11 homffn ⊢ 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
13 12 a1i ⊢ ( 𝜑 → 𝐻 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
14 5 13 4 ssc1 ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
15 2 11 6 5 14 rescbas ⊢ ( 𝜑 → 𝑆 = ( Base ‘ 𝐷 ) )
16 2 11 6 5 14 reschom ⊢ ( 𝜑 → 𝐽 = ( Hom ‘ 𝐷 ) )
17 2 11 6 5 14 3 rescco ⊢ ( 𝜑 → · = ( comp ‘ 𝐷 ) )
18 2 ovexi ⊢ 𝐷 ∈ V
19 18 a1i ⊢ ( 𝜑 → 𝐷 ∈ V )
20 biid ⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) )
21 oveq2 ⊢ ( 𝑚 = 𝑓 → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) = ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) )
22 id ⊢ ( 𝑚 = 𝑓 → 𝑚 = 𝑓 )
23 21 22 eqeq12d ⊢ ( 𝑚 = 𝑓 → ( ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) = 𝑚 ↔ ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 ) )
24 oveq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 𝐽 𝑏 ) = ( 𝑥 𝐽 𝑏 ) )
25 opeq1 ⊢ ( 𝑎 = 𝑥 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑏 ⟩ )
26 25 oveq1d ⊢ ( 𝑎 = 𝑥 → ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) = ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) )
27 26 oveqd ⊢ ( 𝑎 = 𝑥 → ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) )
28 27 eqeq1d ⊢ ( 𝑎 = 𝑥 → ( ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ↔ ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ) )
29 24 28 raleqbidv ⊢ ( 𝑎 = 𝑥 → ( ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ↔ ∀ 𝑚 ∈ ( 𝑥 𝐽 𝑏 ) ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ) )
30 oveq2 ⊢ ( 𝑏 = 𝑦 → ( 𝑥 𝐽 𝑏 ) = ( 𝑥 𝐽 𝑦 ) )
31 opeq2 ⊢ ( 𝑏 = 𝑦 → ⟨ 𝑥 , 𝑏 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
32 id ⊢ ( 𝑏 = 𝑦 → 𝑏 = 𝑦 )
33 31 32 oveq12d ⊢ ( 𝑏 = 𝑦 → ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) = ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) )
34 33 oveqd ⊢ ( 𝑏 = 𝑦 → ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) )
35 34 eqeq1d ⊢ ( 𝑏 = 𝑦 → ( ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ↔ ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) = 𝑚 ) )
36 30 35 raleqbidv ⊢ ( 𝑏 = 𝑦 → ( ∀ 𝑚 ∈ ( 𝑥 𝐽 𝑏 ) ( 1 ( ⟨ 𝑥 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 ↔ ∀ 𝑚 ∈ ( 𝑥 𝐽 𝑦 ) ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) = 𝑚 ) )
37 8 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 1 ( ⟨ 𝑎 , 𝑏 ⟩ · 𝑏 ) 𝑚 ) = 𝑚 )
39 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑥 ∈ 𝑆 )
40 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑦 ∈ 𝑆 )
41 29 36 38 39 40 rspc2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ∀ 𝑚 ∈ ( 𝑥 𝐽 𝑦 ) ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑚 ) = 𝑚 )
42 simpr31 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) )
43 23 41 42 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 1 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
44 oveq1 ⊢ ( 𝑚 = 𝑔 → ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) )
45 id ⊢ ( 𝑚 = 𝑔 → 𝑚 = 𝑔 )
46 44 45 eqeq12d ⊢ ( 𝑚 = 𝑔 → ( ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑚 ↔ ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 ) )
47 oveq1 ⊢ ( 𝑎 = 𝑦 → ( 𝑎 𝐽 𝑏 ) = ( 𝑦 𝐽 𝑏 ) )
48 id ⊢ ( 𝑎 = 𝑦 → 𝑎 = 𝑦 )
49 48 48 opeq12d ⊢ ( 𝑎 = 𝑦 → ⟨ 𝑎 , 𝑎 ⟩ = ⟨ 𝑦 , 𝑦 ⟩ )
50 49 oveq1d ⊢ ( 𝑎 = 𝑦 → ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) = ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) )
51 50 oveqd ⊢ ( 𝑎 = 𝑦 → ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) )
52 51 eqeq1d ⊢ ( 𝑎 = 𝑦 → ( ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 ↔ ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) = 𝑚 ) )
53 47 52 raleqbidv ⊢ ( 𝑎 = 𝑦 → ( ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 ↔ ∀ 𝑚 ∈ ( 𝑦 𝐽 𝑏 ) ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) = 𝑚 ) )
54 oveq2 ⊢ ( 𝑏 = 𝑧 → ( 𝑦 𝐽 𝑏 ) = ( 𝑦 𝐽 𝑧 ) )
55 oveq2 ⊢ ( 𝑏 = 𝑧 → ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) = ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) )
56 55 oveqd ⊢ ( 𝑏 = 𝑧 → ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) = ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) )
57 56 eqeq1d ⊢ ( 𝑏 = 𝑧 → ( ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) = 𝑚 ↔ ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑚 ) )
58 54 57 raleqbidv ⊢ ( 𝑏 = 𝑧 → ( ∀ 𝑚 ∈ ( 𝑦 𝐽 𝑏 ) ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑏 ) 1 ) = 𝑚 ↔ ∀ 𝑚 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑚 ) )
59 9 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 )
60 59 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ∀ 𝑚 ∈ ( 𝑎 𝐽 𝑏 ) ( 𝑚 ( ⟨ 𝑎 , 𝑎 ⟩ · 𝑏 ) 1 ) = 𝑚 )
61 simpr2l ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑧 ∈ 𝑆 )
62 53 58 60 40 61 rspc2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ∀ 𝑚 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑚 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑚 )
63 simpr32 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) )
64 46 62 63 rspcdva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 1 ) = 𝑔 )
65 simpl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝜑 )
66 65 39 40 61 42 63 10 syl132anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) )
67 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
68 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝐶 ∈ Cat )
69 14 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
70 69 39 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
71 69 40 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
72 69 61 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
73 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝐽 Fn ( 𝑆 × 𝑆 ) )
74 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝐽 ⊆cat 𝐻 )
75 73 74 39 40 ssc2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑥 𝐽 𝑦 ) ⊆ ( 𝑥 𝐻 𝑦 ) )
76 75 42 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
77 1 11 67 70 71 homfval ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
78 76 77 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
79 73 74 40 61 ssc2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑦 𝐽 𝑧 ) ⊆ ( 𝑦 𝐻 𝑧 ) )
80 79 63 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
81 1 11 67 71 72 homfval ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑦 𝐻 𝑧 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
82 80 81 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
83 simpr2r ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑤 ∈ 𝑆 )
84 69 83 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
85 73 74 61 83 ssc2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑧 𝐽 𝑤 ) ⊆ ( 𝑧 𝐻 𝑤 ) )
86 simpr33 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) )
87 85 86 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) )
88 1 11 67 72 84 homfval ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( 𝑧 𝐻 𝑤 ) = ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
89 87 88 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 ( Hom ‘ 𝐶 ) 𝑤 ) )
90 11 67 3 68 70 71 72 78 82 84 89 catass ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐽 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
91 15 16 17 19 20 7 43 64 66 90 iscatd2 ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑦 ∈ 𝑆 ↦ 1 ) ) )