This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcfn2

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

Ref Expression
Hypotheses funcfn2.b ⊢ B = Base D
funcfn2.f ⊢ φ → F D Func E G
Assertion funcfn2 ⊢ φ → G Fn B × B

Proof

Step Hyp Ref Expression
1 funcfn2.b ⊢ B = Base D
2 funcfn2.f ⊢ φ → F D Func E G
3 eqid ⊢ Hom ⁡ D = Hom ⁡ D
4 eqid ⊢ Hom ⁡ E = Hom ⁡ E
5 1 3 4 2 funcixp ⊢ φ → G ∈ ⨉ x ∈ B × B F ⁡ 1 st ⁡ x Hom ⁡ E F ⁡ 2 nd ⁡ x Hom ⁡ D ⁡ x
6 ixpfn ⊢ G ∈ ⨉ x ∈ B × B F ⁡ 1 st ⁡ x Hom ⁡ E F ⁡ 2 nd ⁡ x Hom ⁡ D ⁡ x → G Fn B × B
7 5 6 syl ⊢ φ → G Fn B × B