Metamath Proof Explorer


Theorem reschomf

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 reschomf φ 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 1 2 3 4 5 reschom φ H = Hom D
7 1 2 3 4 5 rescbas φ S = Base D
8 7 sqxpeqd φ S × S = Base D × Base D
9 6 8 fneq12d φ H Fn S × S Hom D Fn Base D × Base D
10 4 9 mpbid φ Hom D Fn Base D × Base D
11 fnov Hom D Fn Base D × Base D Hom D = x Base D , y Base D x Hom D y
12 10 11 sylib φ Hom D = x Base D , y Base D x Hom D y
13 6 12 eqtrd φ H = x Base D , y Base D x Hom D y
14 eqid Hom 𝑓 D = Hom 𝑓 D
15 eqid Base D = Base D
16 eqid Hom D = Hom D
17 14 15 16 homffval Hom 𝑓 D = x Base D , y Base D x Hom D y
18 13 17 eqtr4di φ H = Hom 𝑓 D