Metamath Proof Explorer

Theorem natixp

Description: A natural transformation is a function from the objects of C to homomorphisms from F ( x ) to G ( x ) . (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
Assertion natixp ⊢ φ → A ∈ ⨉ x ∈ B 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 eqid ⊢ Hom ⁡ C = Hom ⁡ C
6 eqid ⊢ comp ⁡ D = comp ⁡ D
7 1 natrcl ⊢ A ∈ F G N K L → F G ∈ C Func D ∧ K L ∈ C Func D
8 2 7 syl ⊢ φ → F G ∈ C Func D ∧ K L ∈ C Func D
9 8 simpld ⊢ φ → F G ∈ C Func D
10 df-br ⊢ F C Func D G ↔ F G ∈ C Func D
11 9 10 sylibr ⊢ φ → F C Func D G
12 8 simprd ⊢ φ → K L ∈ C Func D
13 df-br ⊢ K C Func D L ↔ K L ∈ C Func D
14 12 13 sylibr ⊢ φ → K C Func D L
15 1 3 5 4 6 11 14 isnat ⊢ φ → A ∈ F G N K L ↔ A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x Hom ⁡ C y A ⁡ y F ⁡ x F ⁡ y comp ⁡ D K ⁡ y x G y ⁡ z = x L y ⁡ z F ⁡ x K ⁡ x comp ⁡ D K ⁡ y A ⁡ x
16 2 15 mpbid ⊢ φ → A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x ∧ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ x Hom ⁡ C y A ⁡ y F ⁡ x F ⁡ y comp ⁡ D K ⁡ y x G y ⁡ z = x L y ⁡ z F ⁡ x K ⁡ x comp ⁡ D K ⁡ y A ⁡ x
17 16 simpld ⊢ φ → A ∈ ⨉ x ∈ B F ⁡ x J K ⁡ x