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