Metamath Proof Explorer

Theorem funcixp

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

Ref Expression
Hypotheses funcixp.b ⊢ B = Base D
funcixp.h ⊢ H = Hom ⁡ D
funcixp.j ⊢ J = Hom ⁡ E
funcixp.f ⊢ φ → F D Func E G
Assertion funcixp ⊢ φ → G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z

Proof

Step Hyp Ref Expression
1 funcixp.b ⊢ B = Base D
2 funcixp.h ⊢ H = Hom ⁡ D
3 funcixp.j ⊢ J = Hom ⁡ E
4 funcixp.f ⊢ φ → F D Func E G
5 eqid ⊢ Base E = Base 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 4 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 5 2 3 6 7 8 9 14 15 isfunc ⊢ φ → F D Func E G ↔ F : B ⟶ Base E ∧ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ∧ ∀ x ∈ B x G x ⁡ Id ⁡ D ⁡ x = Id ⁡ E ⁡ F ⁡ x ∧ ∀ y ∈ B ∀ z ∈ B ∀ m ∈ x H y ∀ n ∈ y H 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 4 16 mpbid ⊢ φ → F : B ⟶ Base E ∧ G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z ∧ ∀ x ∈ B x G x ⁡ Id ⁡ D ⁡ x = Id ⁡ E ⁡ F ⁡ x ∧ ∀ y ∈ B ∀ z ∈ B ∀ m ∈ x H y ∀ n ∈ y H 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 simp2d ⊢ φ → G ∈ ⨉ z ∈ B × B F ⁡ 1 st ⁡ z J F ⁡ 2 nd ⁡ z H ⁡ z