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	$⊢ φ \to A \in (⟨F, G⟩ N ⟨K, L⟩)$
		natixp.b	$⊢ B = {Base}_{C}$
		natixp.j	$⊢ J = Hom (D)$
	Assertion	natixp	$⊢ φ \to A \in \underset{x \in B}{⨉} (F (x) J K (x))$

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	$⊢ N = C Nat D$
2		natixp.2	$⊢ φ \to A \in (⟨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 \in (⟨F, G⟩ N ⟨K, L⟩) \to (⟨F, G⟩ \in (C Func D) \land ⟨K, L⟩ \in (C Func D))$
8	2 7	syl	$⊢ φ \to (⟨F, G⟩ \in (C Func D) \land ⟨K, L⟩ \in (C Func D))$
9	8	simpld	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
10		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
11	9 10	sylibr	$⊢ φ \to F (C Func D) G$
12	8	simprd	$⊢ φ \to ⟨K, L⟩ \in (C Func D)$
13		df-br	$⊢ K (C Func D) L \leftrightarrow ⟨K, L⟩ \in (C Func D)$
14	12 13	sylibr	$⊢ φ \to K (C Func D) L$
15	1 3 5 4 6 11 14	isnat	$⊢ φ \to (A \in (⟨F, G⟩ N ⟨K, L⟩) \leftrightarrow (A \in \underset{x \in B}{⨉} (F (x) J K (x)) \land \forall x \in B \forall y \in B \forall z \in (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	$⊢ φ \to (A \in \underset{x \in B}{⨉} (F (x) J K (x)) \land \forall x \in B \forall y \in B \forall z \in (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	$⊢ φ \to A \in \underset{x \in B}{⨉} (F (x) J K (x))$