natrcl

Description: Reverse closure for a natural transformation. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Hypothesis	natrcl.1	$⊢ N = C Nat D$
	Assertion	natrcl	$⊢ A \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$

Step	Hyp	Ref	Expression
1		natrcl.1	$⊢ N = C Nat D$
2		eqid	$⊢ {Base}_{C} = {Base}_{C}$
3		eqid	$⊢ Hom (C) = Hom (C)$
4		eqid	$⊢ Hom (D) = Hom (D)$
5		eqid	$⊢ comp (D) = comp (D)$
6	1 2 3 4 5	natfval	$⊢ N = (f \in (C Func D), g \in (C Func D) ⟼ ⦋ 1^{st} (f) / r ⦌ ⦋ 1^{st} (g) / s ⦌ \{a \in \underset{x \in {Base}_{C}}{⨉} (r (x) Hom (D) s (x)) \| \forall x \in {Base}_{C} \forall y \in {Base}_{C} \forall h \in (x Hom (C) y) a (y) (⟨r (x), r (y)⟩ comp (D) s (y)) (x 2^{nd} (f) y) (h) = (x 2^{nd} (g) y) (h) (⟨r (x), s (x)⟩ comp (D) s (y)) a (x)\})$
7	6	elmpocl	$⊢ A \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$

Metamath Proof Explorer