This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑥 ) ) ) )