Metamath Proof Explorer

Theorem reschom

Description: Hom-sets of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses rescbas.d ⊢ D = C ↾ cat H
rescbas.b ⊢ B = Base C
rescbas.c ⊢ φ → C ∈ V
rescbas.h ⊢ φ → H Fn S × S
rescbas.s ⊢ φ → S ⊆ B
Assertion reschom ⊢ φ → H = Hom ⁡ D

Proof

Step Hyp Ref Expression
1 rescbas.d ⊢ D = C ↾ cat H
2 rescbas.b ⊢ B = Base C
3 rescbas.c ⊢ φ → C ∈ V
4 rescbas.h ⊢ φ → H Fn S × S
5 rescbas.s ⊢ φ → S ⊆ B
6 ovex ⊢ C ↾ 𝑠 S ∈ V
7 2 fvexi ⊢ B ∈ V
8 7 ssex ⊢ S ⊆ B → S ∈ V
9 5 8 syl ⊢ φ → S ∈ V
10 9 9 xpexd ⊢ φ → S × S ∈ V
11 fnex ⊢ H Fn S × S ∧ S × S ∈ V → H ∈ V
12 4 10 11 syl2anc ⊢ φ → H ∈ V
13 homid ⊢ Hom = Slot Hom ⁡ ndx
14 13 setsid ⊢ C ↾ 𝑠 S ∈ V ∧ H ∈ V → H = Hom ⁡ C ↾ 𝑠 S sSet Hom ⁡ ndx H
15 6 12 14 sylancr ⊢ φ → H = Hom ⁡ C ↾ 𝑠 S sSet Hom ⁡ ndx H
16 1 3 9 4 rescval2 ⊢ φ → D = C ↾ 𝑠 S sSet Hom ⁡ ndx H
17 16 fveq2d ⊢ φ → Hom ⁡ D = Hom ⁡ C ↾ 𝑠 S sSet Hom ⁡ ndx H
18 15 17 eqtr4d ⊢ φ → H = Hom ⁡ D