Metamath Proof Explorer


Theorem funcf1

Description: The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcf1.b B = Base D
funcf1.c C = Base E
funcf1.f φ F D Func E G
Assertion funcf1 φ F : B C

Proof

Step Hyp Ref Expression
1 funcf1.b B = Base D
2 funcf1.c C = Base E
3 funcf1.f φ F D Func E G
4 eqid Hom D = Hom D
5 eqid Hom E = Hom E
6 eqid Id D = Id D
7 eqid Id E = Id E
8 eqid comp D = comp D
9 eqid comp E = comp E
10 df-br F D Func E G F G D Func E
11 3 10 sylib φ F G D Func E
12 funcrcl F G D Func E D Cat E Cat
13 11 12 syl φ D Cat E Cat
14 13 simpld φ D Cat
15 13 simprd φ E Cat
16 1 2 4 5 6 7 8 9 14 15 isfunc φ F D Func E G F : B C G z B × B F 1 st z Hom E F 2 nd z Hom D z x B x G x Id D x = Id E F x y B z B m x Hom D y n y Hom D z x G z n x y comp D z m = y G z n F x F y comp E F z x G y m
17 3 16 mpbid φ F : B C G z B × B F 1 st z Hom E F 2 nd z Hom D z x B x G x Id D x = Id E F x y B z B m x Hom D y n y Hom D z x G z n x y comp D z m = y G z n F x F y comp E F z x G y m
18 17 simp1d φ F : B C