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

Metamath Proof Explorer

Theorem natfn

Description: A natural transformation is a function on the objects of C . (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses natrcl.1 ⊢ N = C Nat D
natixp.2 ⊢ φ → A ∈ F G N K L
natixp.b ⊢ B = Base C
Assertion natfn ⊢ φ → A Fn B

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ N = C Nat D
2 natixp.2 ⊢ φ → A ∈ F G N K L
3 natixp.b ⊢ B = Base C
4 eqid ⊢ Hom ⁡ D = Hom ⁡ D
5 1 2 3 4 natixp ⊢ φ → A ∈ ⨉ x ∈ B F ⁡ x Hom ⁡ D K ⁡ x
6 ixpfn ⊢ A ∈ ⨉ x ∈ B F ⁡ x Hom ⁡ D K ⁡ x → A Fn B
7 5 6 syl ⊢ φ → A Fn B