| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | resscatc.d | . . . . . 6
⊢ 𝐷 = (CatCat‘𝑉) | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 3 |  | resscatc.1 | . . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑊) | 
| 4 |  | resscatc.2 | . . . . . . . 8
⊢ (𝜑 → 𝑉 ⊆ 𝑈) | 
| 5 | 3, 4 | ssexd 5324 | . . . . . . 7
⊢ (𝜑 → 𝑉 ∈ V) | 
| 6 | 5 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑉 ∈ V) | 
| 7 |  | eqid 2737 | . . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 8 |  | simprl 771 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑥 ∈ (𝑉 ∩ Cat)) | 
| 9 | 1, 2, 5 | catcbas 18146 | . . . . . . . 8
⊢ (𝜑 → (Base‘𝐷) = (𝑉 ∩ Cat)) | 
| 10 | 9 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (Base‘𝐷) = (𝑉 ∩ Cat)) | 
| 11 | 8, 10 | eleqtrrd 2844 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑥 ∈ (Base‘𝐷)) | 
| 12 |  | simprr 773 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑦 ∈ (𝑉 ∩ Cat)) | 
| 13 | 12, 10 | eleqtrrd 2844 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑦 ∈ (Base‘𝐷)) | 
| 14 | 1, 2, 6, 7, 11, 13 | catchom 18148 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥 Func 𝑦)) | 
| 15 |  | resscatc.c | . . . . . 6
⊢ 𝐶 = (CatCat‘𝑈) | 
| 16 |  | eqid 2737 | . . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 17 | 3 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑈 ∈ 𝑊) | 
| 18 |  | eqid 2737 | . . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 19 |  | inass 4228 | . . . . . . . . . . 11
⊢ ((𝑉 ∩ 𝑈) ∩ Cat) = (𝑉 ∩ (𝑈 ∩ Cat)) | 
| 20 | 15, 16, 3 | catcbas 18146 | . . . . . . . . . . . 12
⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Cat)) | 
| 21 | 20 | ineq2d 4220 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑉 ∩ (Base‘𝐶)) = (𝑉 ∩ (𝑈 ∩ Cat))) | 
| 22 | 19, 21 | eqtr4id 2796 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑉 ∩ 𝑈) ∩ Cat) = (𝑉 ∩ (Base‘𝐶))) | 
| 23 |  | dfss2 3969 | . . . . . . . . . . . 12
⊢ (𝑉 ⊆ 𝑈 ↔ (𝑉 ∩ 𝑈) = 𝑉) | 
| 24 | 4, 23 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑉 ∩ 𝑈) = 𝑉) | 
| 25 | 24 | ineq1d 4219 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑉 ∩ 𝑈) ∩ Cat) = (𝑉 ∩ Cat)) | 
| 26 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝐶 ↾s 𝑉) = (𝐶 ↾s 𝑉) | 
| 27 | 26, 16 | ressbas 17280 | . . . . . . . . . . 11
⊢ (𝑉 ∈ V → (𝑉 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑉))) | 
| 28 | 5, 27 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑉 ∩ (Base‘𝐶)) = (Base‘(𝐶 ↾s 𝑉))) | 
| 29 | 22, 25, 28 | 3eqtr3d 2785 | . . . . . . . . 9
⊢ (𝜑 → (𝑉 ∩ Cat) = (Base‘(𝐶 ↾s 𝑉))) | 
| 30 | 26, 16 | ressbasss 17284 | . . . . . . . . 9
⊢
(Base‘(𝐶
↾s 𝑉))
⊆ (Base‘𝐶) | 
| 31 | 29, 30 | eqsstrdi 4028 | . . . . . . . 8
⊢ (𝜑 → (𝑉 ∩ Cat) ⊆ (Base‘𝐶)) | 
| 32 | 31 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (𝑉 ∩ Cat) ⊆ (Base‘𝐶)) | 
| 33 | 32, 8 | sseldd 3984 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑥 ∈ (Base‘𝐶)) | 
| 34 | 32, 12 | sseldd 3984 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → 𝑦 ∈ (Base‘𝐶)) | 
| 35 | 15, 16, 17, 18, 33, 34 | catchom 18148 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥 Func 𝑦)) | 
| 36 | 26, 18 | resshom 17463 | . . . . . . 7
⊢ (𝑉 ∈ V → (Hom
‘𝐶) = (Hom
‘(𝐶
↾s 𝑉))) | 
| 37 | 5, 36 | syl 17 | . . . . . 6
⊢ (𝜑 → (Hom ‘𝐶) = (Hom ‘(𝐶 ↾s 𝑉))) | 
| 38 | 37 | oveqdr 7459 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘(𝐶 ↾s 𝑉))𝑦)) | 
| 39 | 14, 35, 38 | 3eqtr2rd 2784 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat))) → (𝑥(Hom ‘(𝐶 ↾s 𝑉))𝑦) = (𝑥(Hom ‘𝐷)𝑦)) | 
| 40 | 39 | ralrimivva 3202 | . . 3
⊢ (𝜑 → ∀𝑥 ∈ (𝑉 ∩ Cat)∀𝑦 ∈ (𝑉 ∩ Cat)(𝑥(Hom ‘(𝐶 ↾s 𝑉))𝑦) = (𝑥(Hom ‘𝐷)𝑦)) | 
| 41 |  | eqid 2737 | . . . 4
⊢ (Hom
‘(𝐶
↾s 𝑉)) =
(Hom ‘(𝐶
↾s 𝑉)) | 
| 42 | 9 | eqcomd 2743 | . . . 4
⊢ (𝜑 → (𝑉 ∩ Cat) = (Base‘𝐷)) | 
| 43 | 41, 7, 29, 42 | homfeq 17737 | . . 3
⊢ (𝜑 → ((Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷) ↔ ∀𝑥 ∈ (𝑉 ∩ Cat)∀𝑦 ∈ (𝑉 ∩ Cat)(𝑥(Hom ‘(𝐶 ↾s 𝑉))𝑦) = (𝑥(Hom ‘𝐷)𝑦))) | 
| 44 | 40, 43 | mpbird 257 | . 2
⊢ (𝜑 → (Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷)) | 
| 45 | 5 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑉 ∈ V) | 
| 46 |  | eqid 2737 | . . . . . . . 8
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 47 |  | simplr1 1216 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑥 ∈ (𝑉 ∩ Cat)) | 
| 48 | 9 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (Base‘𝐷) = (𝑉 ∩ Cat)) | 
| 49 | 47, 48 | eleqtrrd 2844 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑥 ∈ (Base‘𝐷)) | 
| 50 |  | simplr2 1217 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑦 ∈ (𝑉 ∩ Cat)) | 
| 51 | 50, 48 | eleqtrrd 2844 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑦 ∈ (Base‘𝐷)) | 
| 52 |  | simplr3 1218 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑧 ∈ (𝑉 ∩ Cat)) | 
| 53 | 52, 48 | eleqtrrd 2844 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑧 ∈ (Base‘𝐷)) | 
| 54 |  | simprl 771 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)) | 
| 55 | 1, 2, 45, 7, 49, 51 | catchom 18148 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥 Func 𝑦)) | 
| 56 | 54, 55 | eleqtrd 2843 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑓 ∈ (𝑥 Func 𝑦)) | 
| 57 |  | simprr 773 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) | 
| 58 | 1, 2, 45, 7, 51, 53 | catchom 18148 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑦(Hom ‘𝐷)𝑧) = (𝑦 Func 𝑧)) | 
| 59 | 57, 58 | eleqtrd 2843 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑔 ∈ (𝑦 Func 𝑧)) | 
| 60 | 1, 2, 45, 46, 49, 51, 53, 56, 59 | catcco 18150 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) = (𝑔 ∘func 𝑓)) | 
| 61 | 3 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑈 ∈ 𝑊) | 
| 62 |  | eqid 2737 | . . . . . . . 8
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 63 | 31 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑉 ∩ Cat) ⊆ (Base‘𝐶)) | 
| 64 | 63, 47 | sseldd 3984 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑥 ∈ (Base‘𝐶)) | 
| 65 | 63, 50 | sseldd 3984 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑦 ∈ (Base‘𝐶)) | 
| 66 | 63, 52 | sseldd 3984 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → 𝑧 ∈ (Base‘𝐶)) | 
| 67 | 15, 16, 61, 62, 64, 65, 66, 56, 59 | catcco 18150 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (𝑔 ∘func 𝑓)) | 
| 68 | 26, 62 | ressco 17464 | . . . . . . . . . . 11
⊢ (𝑉 ∈ V →
(comp‘𝐶) =
(comp‘(𝐶
↾s 𝑉))) | 
| 69 | 5, 68 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (comp‘𝐶) = (comp‘(𝐶 ↾s 𝑉))) | 
| 70 | 69 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (comp‘𝐶) = (comp‘(𝐶 ↾s 𝑉))) | 
| 71 | 70 | oveqd 7448 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (〈𝑥, 𝑦〉(comp‘𝐶)𝑧) = (〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)) | 
| 72 | 71 | oveqd 7448 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)𝑓)) | 
| 73 | 60, 67, 72 | 3eqtr2d 2783 | . . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)𝑓)) | 
| 74 | 73 | ralrimivva 3202 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑉 ∩ Cat) ∧ 𝑦 ∈ (𝑉 ∩ Cat) ∧ 𝑧 ∈ (𝑉 ∩ Cat))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)𝑓)) | 
| 75 | 74 | ralrimivvva 3205 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ (𝑉 ∩ Cat)∀𝑦 ∈ (𝑉 ∩ Cat)∀𝑧 ∈ (𝑉 ∩ Cat)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)𝑓)) | 
| 76 |  | eqid 2737 | . . . . 5
⊢
(comp‘(𝐶
↾s 𝑉)) =
(comp‘(𝐶
↾s 𝑉)) | 
| 77 | 44 | eqcomd 2743 | . . . . 5
⊢ (𝜑 → (Homf
‘𝐷) =
(Homf ‘(𝐶 ↾s 𝑉))) | 
| 78 | 46, 76, 7, 42, 29, 77 | comfeq 17749 | . . . 4
⊢ (𝜑 →
((compf‘𝐷) = (compf‘(𝐶 ↾s 𝑉)) ↔ ∀𝑥 ∈ (𝑉 ∩ Cat)∀𝑦 ∈ (𝑉 ∩ Cat)∀𝑧 ∈ (𝑉 ∩ Cat)∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)(𝑔(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑓) = (𝑔(〈𝑥, 𝑦〉(comp‘(𝐶 ↾s 𝑉))𝑧)𝑓))) | 
| 79 | 75, 78 | mpbird 257 | . . 3
⊢ (𝜑 →
(compf‘𝐷) = (compf‘(𝐶 ↾s 𝑉))) | 
| 80 | 79 | eqcomd 2743 | . 2
⊢ (𝜑 →
(compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)) | 
| 81 | 44, 80 | jca 511 | 1
⊢ (𝜑 → ((Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷) ∧
(compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷))) |