fuco23alem

Description: The naturality property ( nati ) in category E . (Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fuco23a.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
	fuco23a.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
	fuco23a.x	$⊢ φ \to X \in {Base}_{C}$
	fuco23alem.o	$⊢ \underset{˙}{\cdot} = comp (E)$
Assertion	fuco23alem	$⊢ φ \to B (M (X)) (⟨K (F (X)), K (M (X))⟩ \underset{˙}{\cdot} R (M (X))) (F (X) L M (X)) (A (X)) = (F (X) S M (X)) (A (X)) (⟨K (F (X)), R (F (X))⟩ \underset{˙}{\cdot} R (M (X))) B (F (X))$

Step	Hyp	Ref	Expression
1		fuco23a.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
2		fuco23a.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
3		fuco23a.x	$⊢ φ \to X \in {Base}_{C}$
4		fuco23alem.o	$⊢ \underset{˙}{\cdot} = comp (E)$
5		eqid	$⊢ D Nat E = D Nat E$
6		eqid	$⊢ {Base}_{D} = {Base}_{D}$
7		eqid	$⊢ Hom (D) = Hom (D)$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		eqid	$⊢ C Nat D = C Nat D$
10	9 1	natrcl2	$⊢ φ \to F (C Func D) G$
11	8 6 10	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
12	11 3	ffvelcdmd	$⊢ φ \to F (X) \in {Base}_{D}$
13	9 1	natrcl3	$⊢ φ \to M (C Func D) N$
14	8 6 13	funcf1	$⊢ φ \to M : {Base}_{C} ⟶ {Base}_{D}$
15	14 3	ffvelcdmd	$⊢ φ \to M (X) \in {Base}_{D}$
16	9 1 8 7 3	natcl	$⊢ φ \to A (X) \in (F (X) Hom (D) M (X))$
17	5 2 6 7 4 12 15 16	nati	$⊢ φ \to B (M (X)) (⟨K (F (X)), K (M (X))⟩ \underset{˙}{\cdot} R (M (X))) (F (X) L M (X)) (A (X)) = (F (X) S M (X)) (A (X)) (⟨K (F (X)), R (F (X))⟩ \underset{˙}{\cdot} R (M (X))) B (F (X))$

Metamath Proof Explorer