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

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