Metamath Proof Explorer

Theorem resscatc

Description: The restriction of the category of categories to a subset is the category of categories in the subset. Thus, the CatCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses resscatc.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
resscatc.d ⊢ 𝐷 = ( CatCat ‘ 𝑉 )
resscatc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
resscatc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
Assertion resscatc ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 resscatc.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 resscatc.d ⊢ 𝐷 = ( CatCat ‘ 𝑉 )
3 resscatc.1 ⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
4 resscatc.2 ⊢ ( 𝜑 → 𝑉 ⊆ 𝑈 )
5 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6 3 4 ssexd ⊢ ( 𝜑 → 𝑉 ∈ V )
7 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑉 ∈ V )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑥 ∈ ( 𝑉 ∩ Cat ) )
10 2 5 6 catcbas ⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( 𝑉 ∩ Cat ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( Base ‘ 𝐷 ) = ( 𝑉 ∩ Cat ) )
12 9 11 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑦 ∈ ( 𝑉 ∩ Cat ) )
14 13 11 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
15 2 5 7 8 12 14 catchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 Func 𝑦 ) )
16 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑈 ∈ 𝑊 )
18 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
19 inass ⊢ ( ( 𝑉 ∩ 𝑈 ) ∩ Cat ) = ( 𝑉 ∩ ( 𝑈 ∩ Cat ) )
20 1 16 3 catcbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Cat ) )
21 20 ineq2d ⊢ ( 𝜑 → ( 𝑉 ∩ ( Base ‘ 𝐶 ) ) = ( 𝑉 ∩ ( 𝑈 ∩ Cat ) ) )
22 19 21 eqtr4id ⊢ ( 𝜑 → ( ( 𝑉 ∩ 𝑈 ) ∩ Cat ) = ( 𝑉 ∩ ( Base ‘ 𝐶 ) ) )
23 dfss2 ⊢ ( 𝑉 ⊆ 𝑈 ↔ ( 𝑉 ∩ 𝑈 ) = 𝑉 )
24 4 23 sylib ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑈 ) = 𝑉 )
25 24 ineq1d ⊢ ( 𝜑 → ( ( 𝑉 ∩ 𝑈 ) ∩ Cat ) = ( 𝑉 ∩ Cat ) )
26 eqid ⊢ ( 𝐶 ↾s 𝑉 ) = ( 𝐶 ↾s 𝑉 )
27 26 16 ressbas ⊢ ( 𝑉 ∈ V → ( 𝑉 ∩ ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) )
28 6 27 syl ⊢ ( 𝜑 → ( 𝑉 ∩ ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) )
29 22 25 28 3eqtr3d ⊢ ( 𝜑 → ( 𝑉 ∩ Cat ) = ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) )
30 26 16 ressbasss ⊢ ( Base ‘ ( 𝐶 ↾s 𝑉 ) ) ⊆ ( Base ‘ 𝐶 )
31 29 30 eqsstrdi ⊢ ( 𝜑 → ( 𝑉 ∩ Cat ) ⊆ ( Base ‘ 𝐶 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( 𝑉 ∩ Cat ) ⊆ ( Base ‘ 𝐶 ) )
33 32 9 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
34 32 13 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
35 1 16 17 18 33 34 catchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 Func 𝑦 ) )
36 26 18 resshom ⊢ ( 𝑉 ∈ V → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) )
37 6 36 syl ⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) )
38 37 oveqdr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) )
39 15 35 38 3eqtr2rd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ) ) → ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
40 39 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑦 ∈ ( 𝑉 ∩ Cat ) ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
41 eqid ⊢ ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Hom ‘ ( 𝐶 ↾s 𝑉 ) )
42 10 eqcomd ⊢ ( 𝜑 → ( 𝑉 ∩ Cat ) = ( Base ‘ 𝐷 ) )
43 41 8 29 42 homfeq ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑦 ∈ ( 𝑉 ∩ Cat ) ( 𝑥 ( Hom ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ) )
44 40 43 mpbird ⊢ ( 𝜑 → ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) )
45 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑉 ∈ V )
46 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
47 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑥 ∈ ( 𝑉 ∩ Cat ) )
48 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( Base ‘ 𝐷 ) = ( 𝑉 ∩ Cat ) )
49 47 48 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐷 ) )
50 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑦 ∈ ( 𝑉 ∩ Cat ) )
51 50 48 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
52 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑧 ∈ ( 𝑉 ∩ Cat ) )
53 52 48 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
54 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) )
55 2 5 45 8 49 51 catchom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) = ( 𝑥 Func 𝑦 ) )
56 54 55 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑥 Func 𝑦 ) )
57 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) )
58 2 5 45 8 51 53 catchom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) = ( 𝑦 Func 𝑧 ) )
59 57 58 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑦 Func 𝑧 ) )
60 2 5 45 46 49 51 53 56 59 catcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘func 𝑓 ) )
61 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑈 ∈ 𝑊 )
62 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
63 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑉 ∩ Cat ) ⊆ ( Base ‘ 𝐶 ) )
64 63 47 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
65 63 50 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
66 63 52 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐶 ) )
67 1 16 61 62 64 65 66 56 59 catcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ∘func 𝑓 ) )
68 26 62 ressco ⊢ ( 𝑉 ∈ V → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
69 6 68 syl ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( comp ‘ 𝐶 ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) )
71 70 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) = ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) )
72 71 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
73 60 67 72 3eqtr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) ∧ ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
74 73 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∧ 𝑧 ∈ ( 𝑉 ∩ Cat ) ) ) → ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
75 74 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑧 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) )
76 eqid ⊢ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) = ( comp ‘ ( 𝐶 ↾s 𝑉 ) )
77 44 eqcomd ⊢ ( 𝜑 → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) )
78 46 76 8 42 29 77 comfeq ⊢ ( 𝜑 → ( ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) ↔ ∀ 𝑥 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑦 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑧 ∈ ( 𝑉 ∩ Cat ) ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐷 ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐷 ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( 𝐶 ↾s 𝑉 ) ) 𝑧 ) 𝑓 ) ) )
79 75 78 mpbird ⊢ ( 𝜑 → ( compf ‘ 𝐷 ) = ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) )
80 79 eqcomd ⊢ ( 𝜑 → ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) )
81 44 80 jca ⊢ ( 𝜑 → ( ( Homf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( Homf ‘ 𝐷 ) ∧ ( compf ‘ ( 𝐶 ↾s 𝑉 ) ) = ( compf ‘ 𝐷 ) ) )