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

Metamath Proof Explorer

Theorem natcl

Description: A component of a natural transformation is a morphism. (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
natixp.j ⊢ J = Hom ⁡ D
natcl.1 ⊢ φ → X ∈ B
Assertion natcl ⊢ φ → A ⁡ X ∈ F ⁡ X J K ⁡ X

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 natixp.j ⊢ J = Hom ⁡ D
5 natcl.1 ⊢ φ → X ∈ B
6 1 2 3 4 natixp ⊢ φ → A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x
7 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
8 fveq2 ⊢ x = X → K ⁡ x = K ⁡ X
9 7 8 oveq12d ⊢ x = X → F ⁡ x J K ⁡ x = F ⁡ X J K ⁡ X
10 9 fvixp ⊢ A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x ∧ X ∈ B → A ⁡ X ∈ F ⁡ X J K ⁡ X
11 6 5 10 syl2anc ⊢ φ → A ⁡ X ∈ F ⁡ X J K ⁡ X