Metamath Proof Explorer


Theorem catccatid

Description: Lemma for catccat . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses catccatid.c 𝐶 = ( CatCat ‘ 𝑈 )
catccatid.b 𝐵 = ( Base ‘ 𝐶 )
Assertion catccatid ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( idfunc𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 catccatid.c 𝐶 = ( CatCat ‘ 𝑈 )
2 catccatid.b 𝐵 = ( Base ‘ 𝐶 )
3 2 a1i ( 𝑈𝑉𝐵 = ( Base ‘ 𝐶 ) )
4 eqidd ( 𝑈𝑉 → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
5 eqidd ( 𝑈𝑉 → ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) )
6 1 fvexi 𝐶 ∈ V
7 6 a1i ( 𝑈𝑉𝐶 ∈ V )
8 biid ( ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ↔ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) )
9 id ( 𝑈𝑉𝑈𝑉 )
10 1 2 9 catcbas ( 𝑈𝑉𝐵 = ( 𝑈 ∩ Cat ) )
11 inss2 ( 𝑈 ∩ Cat ) ⊆ Cat
12 10 11 eqsstrdi ( 𝑈𝑉𝐵 ⊆ Cat )
13 12 sselda ( ( 𝑈𝑉𝑥𝐵 ) → 𝑥 ∈ Cat )
14 eqid ( idfunc𝑥 ) = ( idfunc𝑥 )
15 14 idfucl ( 𝑥 ∈ Cat → ( idfunc𝑥 ) ∈ ( 𝑥 Func 𝑥 ) )
16 13 15 syl ( ( 𝑈𝑉𝑥𝐵 ) → ( idfunc𝑥 ) ∈ ( 𝑥 Func 𝑥 ) )
17 simpl ( ( 𝑈𝑉𝑥𝐵 ) → 𝑈𝑉 )
18 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
19 simpr ( ( 𝑈𝑉𝑥𝐵 ) → 𝑥𝐵 )
20 1 2 17 18 19 19 catchom ( ( 𝑈𝑉𝑥𝐵 ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑥 Func 𝑥 ) )
21 16 20 eleqtrrd ( ( 𝑈𝑉𝑥𝐵 ) → ( idfunc𝑥 ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
22 simpl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑈𝑉 )
23 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
24 simpr1l ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑤𝐵 )
25 simpr1r ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑥𝐵 )
26 simpr31 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) )
27 1 2 22 18 24 25 catchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑤 Func 𝑥 ) )
28 26 27 eleqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 Func 𝑥 ) )
29 25 16 syldan ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( idfunc𝑥 ) ∈ ( 𝑥 Func 𝑥 ) )
30 1 2 22 23 24 25 25 28 29 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( idfunc𝑥 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( idfunc𝑥 ) ∘func 𝑓 ) )
31 28 14 cofulid ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( idfunc𝑥 ) ∘func 𝑓 ) = 𝑓 )
32 30 31 eqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( idfunc𝑥 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
33 simpr2l ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑦𝐵 )
34 simpr32 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
35 1 2 22 18 25 33 catchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 Func 𝑦 ) )
36 34 35 eleqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 Func 𝑦 ) )
37 1 2 22 23 25 25 33 29 36 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( idfunc𝑥 ) ) = ( 𝑔func ( idfunc𝑥 ) ) )
38 36 14 cofurid ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔func ( idfunc𝑥 ) ) = 𝑔 )
39 37 38 eqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( idfunc𝑥 ) ) = 𝑔 )
40 28 36 cofucl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔func 𝑓 ) ∈ ( 𝑤 Func 𝑦 ) )
41 1 2 22 23 24 25 33 28 36 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = ( 𝑔func 𝑓 ) )
42 1 2 22 18 24 33 catchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑤 Func 𝑦 ) )
43 40 41 42 3eltr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) )
44 simpr33 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
45 simpr2r ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧𝐵 )
46 1 2 22 18 33 45 catchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) = ( 𝑦 Func 𝑧 ) )
47 44 46 eleqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ∈ ( 𝑦 Func 𝑧 ) )
48 28 36 47 cofuass ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( func 𝑔 ) ∘func 𝑓 ) = ( func ( 𝑔func 𝑓 ) ) )
49 36 47 cofucl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( func 𝑔 ) ∈ ( 𝑥 Func 𝑧 ) )
50 1 2 22 23 24 25 45 28 49 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( func 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( func 𝑔 ) ∘func 𝑓 ) )
51 1 2 22 23 24 33 45 40 47 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔func 𝑓 ) ) = ( func ( 𝑔func 𝑓 ) ) )
52 48 50 51 3eqtr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( func 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔func 𝑓 ) ) )
53 1 2 22 23 25 33 45 36 47 catcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) = ( func 𝑔 ) )
54 53 oveq1d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( func 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
55 41 oveq2d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔func 𝑓 ) ) )
56 52 54 55 3eqtr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝐵𝑥𝐵 ) ∧ ( 𝑦𝐵𝑧𝐵 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
57 3 4 5 7 8 21 32 39 43 56 iscatd2 ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( idfunc𝑥 ) ) ) )