| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (Homf
‘𝐸) =
(Homf ‘𝐸)) | 
| 2 |  | eqidd 2737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) →
(compf‘𝐸) = (compf‘𝐸)) | 
| 3 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 4 |  | eqid 2736 | . . . . . . . . 9
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) | 
| 5 |  | resssetc.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 ∈ 𝑊) | 
| 6 |  | resssetc.c | . . . . . . . . . . . 12
⊢ 𝐶 = (SetCat‘𝑈) | 
| 7 | 6 | setccat 18131 | . . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑊 → 𝐶 ∈ Cat) | 
| 8 | 5, 7 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 9 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝐶 ∈ Cat) | 
| 10 |  | resssetc.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑉 ⊆ 𝑈) | 
| 11 | 6, 5 | setcbas 18124 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) | 
| 12 | 10, 11 | sseqtrd 4019 | . . . . . . . . . 10
⊢ (𝜑 → 𝑉 ⊆ (Base‘𝐶)) | 
| 13 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝑉 ⊆ (Base‘𝐶)) | 
| 14 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝐶 ↾s 𝑉) = (𝐶 ↾s 𝑉) | 
| 15 |  | eqid 2736 | . . . . . . . . 9
⊢ (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉))) = (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉))) | 
| 16 | 3, 4, 9, 13, 14, 15 | fullresc 17897 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → ((Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) ∧
(compf‘(𝐶 ↾s 𝑉)) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))))) | 
| 17 | 16 | simpld 494 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉))))) | 
| 18 |  | resssetc.d | . . . . . . . . . 10
⊢ 𝐷 = (SetCat‘𝑉) | 
| 19 | 6, 18, 5, 10 | resssetc 18138 | . . . . . . . . 9
⊢ (𝜑 → ((Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷) ∧
(compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷))) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → ((Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷) ∧
(compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷))) | 
| 21 | 20 | simpld 494 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (Homf
‘(𝐶
↾s 𝑉)) =
(Homf ‘𝐷)) | 
| 22 | 17, 21 | eqtr3d 2778 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (Homf
‘(𝐶
↾cat ((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) = (Homf ‘𝐷)) | 
| 23 | 16 | simprd 495 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) →
(compf‘(𝐶 ↾s 𝑉)) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉))))) | 
| 24 | 20 | simprd 495 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) →
(compf‘(𝐶 ↾s 𝑉)) = (compf‘𝐷)) | 
| 25 | 23, 24 | eqtr3d 2778 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) →
(compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) = (compf‘𝐷)) | 
| 26 |  | funcrcl 17909 | . . . . . . . 8
⊢ (𝑓 ∈ (𝐸 Func 𝐷) → (𝐸 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 27 | 26 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (𝐸 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 28 | 27 | simpld 494 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝐸 ∈ Cat) | 
| 29 | 3, 4, 9, 13 | fullsubc 17896 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → ((Homf
‘𝐶) ↾ (𝑉 × 𝑉)) ∈ (Subcat‘𝐶)) | 
| 30 | 15, 29 | subccat 17894 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉))) ∈ Cat) | 
| 31 | 27 | simprd 495 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝐷 ∈ Cat) | 
| 32 | 1, 2, 22, 25, 28, 28, 30, 31 | funcpropd 17948 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (𝐸 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) = (𝐸 Func 𝐷)) | 
| 33 |  | funcres2 17944 | . . . . . 6
⊢
(((Homf ‘𝐶) ↾ (𝑉 × 𝑉)) ∈ (Subcat‘𝐶) → (𝐸 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) ⊆ (𝐸 Func 𝐶)) | 
| 34 | 29, 33 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (𝐸 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ (𝑉 × 𝑉)))) ⊆ (𝐸 Func 𝐶)) | 
| 35 | 32, 34 | eqsstrrd 4018 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → (𝐸 Func 𝐷) ⊆ (𝐸 Func 𝐶)) | 
| 36 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝑓 ∈ (𝐸 Func 𝐷)) | 
| 37 | 35, 36 | sseldd 3983 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐸 Func 𝐷)) → 𝑓 ∈ (𝐸 Func 𝐶)) | 
| 38 | 37 | ex 412 | . 2
⊢ (𝜑 → (𝑓 ∈ (𝐸 Func 𝐷) → 𝑓 ∈ (𝐸 Func 𝐶))) | 
| 39 | 38 | ssrdv 3988 | 1
⊢ (𝜑 → (𝐸 Func 𝐷) ⊆ (𝐸 Func 𝐶)) |