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

Metamath Proof Explorer

Theorem setccatid

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

Ref Expression
Hypothesis setccat.c ⊢ 𝐶 = ( SetCat ‘ 𝑈 )
Assertion setccatid ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝑈 ↦ ( I ↾ 𝑥 ) ) ) )

Proof

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