Metamath Proof Explorer


Theorem estrccatid

Description: Lemma for estrccat . (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypothesis estrccat.c 𝐶 = ( ExtStrCat ‘ 𝑈 )
Assertion estrccatid ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 estrccat.c 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 id ( 𝑈𝑉𝑈𝑉 )
3 1 2 estrcbas ( 𝑈𝑉𝑈 = ( 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 f1oi ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) –1-1-onto→ ( Base ‘ 𝑥 )
10 f1of ( ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) –1-1-onto→ ( Base ‘ 𝑥 ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) )
11 9 10 mp1i ( ( 𝑈𝑉𝑥𝑈 ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) )
12 simpl ( ( 𝑈𝑉𝑥𝑈 ) → 𝑈𝑉 )
13 eqid ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14 simpr ( ( 𝑈𝑉𝑥𝑈 ) → 𝑥𝑈 )
15 eqid ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
16 1 12 13 14 14 15 15 elestrchom ( ( 𝑈𝑉𝑥𝑈 ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) ) )
17 11 16 mpbird ( ( 𝑈𝑉𝑥𝑈 ) → ( I ↾ ( Base ‘ 𝑥 ) ) ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
18 simpl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑈𝑉 )
19 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
20 simpr1l ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑤𝑈 )
21 simpr1r ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑥𝑈 )
22 eqid ( Base ‘ 𝑤 ) = ( Base ‘ 𝑤 )
23 simpr31 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) )
24 1 18 13 20 21 22 15 elestrchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) )
25 23 24 mpbid ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) )
26 9 10 mp1i ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( I ↾ ( Base ‘ 𝑥 ) ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑥 ) )
27 1 18 19 20 21 21 22 15 15 25 26 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) )
28 fcoi2 ( 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 )
29 25 28 syl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ∘ 𝑓 ) = 𝑓 )
30 27 29 eqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( I ↾ ( Base ‘ 𝑥 ) ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = 𝑓 )
31 simpr2l ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑦𝑈 )
32 eqid ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
33 simpr32 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
34 1 18 13 21 31 15 32 elestrchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
35 33 34 mpbid ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
36 1 18 19 21 21 31 15 15 32 26 35 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
37 fcoi1 ( 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
38 35 37 syl ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ∘ ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
39 36 38 eqtrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) ( I ↾ ( Base ‘ 𝑥 ) ) ) = 𝑔 )
40 1 18 19 20 21 31 22 15 32 25 35 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) = ( 𝑔𝑓 ) )
41 fco ( ( 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ∧ 𝑓 : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑥 ) ) → ( 𝑔𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) )
42 35 25 41 syl2anc ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) )
43 1 18 13 20 31 22 32 elestrchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ ( 𝑔𝑓 ) : ( Base ‘ 𝑤 ) ⟶ ( Base ‘ 𝑦 ) ) )
44 42 43 mpbird ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) )
45 40 44 eqeltrd ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑦 ) )
46 coass ( ( 𝑔 ) ∘ 𝑓 ) = ( ∘ ( 𝑔𝑓 ) )
47 simpr2r ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → 𝑧𝑈 )
48 eqid ( Base ‘ 𝑧 ) = ( Base ‘ 𝑧 )
49 simpr33 ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) )
50 1 18 13 31 47 32 48 elestrchom ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ↔ : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ) )
51 49 50 mpbid ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) )
52 fco ( ( : ( Base ‘ 𝑦 ) ⟶ ( Base ‘ 𝑧 ) ∧ 𝑔 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) → ( 𝑔 ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑧 ) )
53 51 35 52 syl2anc ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( 𝑔 ) : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑧 ) )
54 1 18 19 20 21 47 22 15 48 25 53 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( 𝑔 ) ∘ 𝑓 ) )
55 1 18 19 20 31 47 22 32 48 42 51 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) = ( ∘ ( 𝑔𝑓 ) ) )
56 46 54 55 3eqtr4a ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) )
57 1 18 19 21 31 47 15 32 48 35 51 estrcco ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) = ( 𝑔 ) )
58 57 oveq1d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) )
59 40 oveq2d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔𝑓 ) ) )
60 56 58 59 3eqtr4d ( ( 𝑈𝑉 ∧ ( ( 𝑤𝑈𝑥𝑈 ) ∧ ( 𝑦𝑈𝑧𝑈 ) ∧ ( 𝑓 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ) ) ) → ( ( ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑔 ) ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ( ⟨ 𝑤 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑤 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
61 3 4 5 7 8 17 30 39 45 60 iscatd2 ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝑈 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )