fuco22natlem

Description: The composed natural transformation is a natural transformation. Use fuco22nat instead. (New usage is discouraged.) (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fuco22natlem.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco22natlem.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
	fuco22natlem.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
	fuco22natlem.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
	fuco22natlem.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
Assertion	fuco22natlem	$⊢ φ \to B (U P V) A \in (O (U) (C Nat E) O (V))$

Proof

Step	Hyp	Ref	Expression
1		fuco22natlem.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
2		fuco22natlem.a	$⊢ φ \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
3		fuco22natlem.b	$⊢ φ \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
4		fuco22natlem.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
5		fuco22natlem.v	$⊢ φ \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
6		eqid	$⊢ C Nat E = C Nat E$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ Hom (E) = Hom (E)$
10		eqid	$⊢ comp (E) = comp (E)$
11		eqid	$⊢ C Nat D = C Nat D$
12	11 2	natrcl2	$⊢ φ \to F (C Func D) G$
13		eqid	$⊢ D Nat E = D Nat E$
14	13 3	natrcl2	$⊢ φ \to K (D Func E) L$
15	1 12 14 4 7	fuco11a	$⊢ φ \to O (U) = ⟨K \circ F, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))⟩$
16	1 12 14 4	fuco11cl	$⊢ φ \to O (U) \in (C Func E)$
17	15 16	eqeltrrd	$⊢ φ \to ⟨K \circ F, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))⟩ \in (C Func E)$
18		df-br	$⊢ (K \circ F) (C Func E) (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) \leftrightarrow ⟨K \circ F, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))⟩ \in (C Func E)$
19	17 18	sylibr	$⊢ φ \to (K \circ F) (C Func E) (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))$
20	11 2	natrcl3	$⊢ φ \to M (C Func D) N$
21	13 3	natrcl3	$⊢ φ \to R (D Func E) S$
22	1 20 21 5 7	fuco11a	$⊢ φ \to O (V) = ⟨R \circ M, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))⟩$
23	1 20 21 5	fuco11cl	$⊢ φ \to O (V) \in (C Func E)$
24	22 23	eqeltrrd	$⊢ φ \to ⟨R \circ M, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))⟩ \in (C Func E)$
25		df-br	$⊢ (R \circ M) (C Func E) (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) \leftrightarrow ⟨R \circ M, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))⟩ \in (C Func E)$
26	24 25	sylibr	$⊢ φ \to (R \circ M) (C Func E) (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))$
27	1 4 5 2 3	fucofn22	$⊢ φ \to (B (U P V) A) Fn {Base}_{C}$
28		eqid	$⊢ {Base}_{E} = {Base}_{E}$
29	14	adantr	$⊢ (φ \land x \in {Base}_{C}) \to K (D Func E) L$
30	29	funcrcl3	$⊢ (φ \land x \in {Base}_{C}) \to E \in Cat$
31		eqid	$⊢ {Base}_{D} = {Base}_{D}$
32	31 28 29	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to K : {Base}_{D} ⟶ {Base}_{E}$
33	12	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F (C Func D) G$
34	7 31 33	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to F : {Base}_{C} ⟶ {Base}_{D}$
35		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
36	34 35	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to F (x) \in {Base}_{D}$
37	32 36	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to K (F (x)) \in {Base}_{E}$
38	20	adantr	$⊢ (φ \land x \in {Base}_{C}) \to M (C Func D) N$
39	7 31 38	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to M : {Base}_{C} ⟶ {Base}_{D}$
40	39 35	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to M (x) \in {Base}_{D}$
41	32 40	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to K (M (x)) \in {Base}_{E}$
42	21	adantr	$⊢ (φ \land x \in {Base}_{C}) \to R (D Func E) S$
43	31 28 42	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to R : {Base}_{D} ⟶ {Base}_{E}$
44	43 40	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to R (M (x)) \in {Base}_{E}$
45		eqid	$⊢ Hom (D) = Hom (D)$
46	31 45 9 29 36 40	funcf2	$⊢ (φ \land x \in {Base}_{C}) \to (F (x) L M (x)) : F (x) Hom (D) M (x) ⟶ K (F (x)) Hom (E) K (M (x))$
47	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
48	11 47 7 45 35	natcl	$⊢ (φ \land x \in {Base}_{C}) \to A (x) \in (F (x) Hom (D) M (x))$
49	46 48	ffvelcdmd	$⊢ (φ \land x \in {Base}_{C}) \to (F (x) L M (x)) (A (x)) \in (K (F (x)) Hom (E) K (M (x)))$
50	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
51	7 31 20	funcf1	$⊢ φ \to M : {Base}_{C} ⟶ {Base}_{D}$
52	51	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to M (x) \in {Base}_{D}$
53	13 50 31 9 52	natcl	$⊢ (φ \land x \in {Base}_{C}) \to B (M (x)) \in (K (M (x)) Hom (E) R (M (x)))$
54	28 9 10 30 37 41 44 49 53	catcocl	$⊢ (φ \land x \in {Base}_{C}) \to B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x)) \in (K (F (x)) Hom (E) R (M (x)))$
55	1	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
56	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
57	5	adantr	$⊢ (φ \land x \in {Base}_{C}) \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
58		eqidd	$⊢ (φ \land x \in {Base}_{C}) \to ⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x)) = ⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))$
59	55 56 57 47 50 35 58	fuco23	$⊢ (φ \land x \in {Base}_{C}) \to (B (U P V) A) (x) = B (M (x)) (⟨K (F (x)), K (M (x))⟩ comp (E) R (M (x))) (F (x) L M (x)) (A (x))$
60	34 35	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (K \circ F) (x) = K (F (x))$
61	39 35	fvco3d	$⊢ (φ \land x \in {Base}_{C}) \to (R \circ M) (x) = R (M (x))$
62	60 61	oveq12d	$⊢ (φ \land x \in {Base}_{C}) \to (K \circ F) (x) Hom (E) (R \circ M) (x) = K (F (x)) Hom (E) R (M (x))$
63	54 59 62	3eltr4d	$⊢ (φ \land x \in {Base}_{C}) \to (B (U P V) A) (x) \in ((K \circ F) (x) Hom (E) (R \circ M) (x))$
64		simplrl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to x \in {Base}_{C}$
65		simplrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to y \in {Base}_{C}$
66	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to A \in (⟨F, G⟩ (C Nat D) ⟨M, N⟩)$
67		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to h \in (x Hom (C) y)$
68	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to B \in (⟨K, L⟩ (D Nat E) ⟨R, S⟩)$
69	1	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ h e. ( x ( Hom ` C ) y ) ) -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
70	4	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
71	5	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to V = ⟨⟨R, S⟩, ⟨M, N⟩⟩$
72	64 65 66 67 68 69 70 71	fuco22natlem3	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (B (U P V) A) (y) (⟨(K \circ F) (x), (K \circ F) (y)⟩ comp (E) (R \circ M) (y)) ((F (x) L F (y)) \circ (x G y)) (h) = ((M (x) S M (y)) \circ (x N y)) (h) (⟨(K \circ F) (x), (R \circ M) (x)⟩ comp (E) (R \circ M) (y)) (B (U P V) A) (x)$
73		fveq2	$⊢ z = x \to F (z) = F (x)$
74	73	oveq1d	$⊢ z = x \to F (z) L F (w) = F (x) L F (w)$
75		oveq1	$⊢ z = x \to z G w = x G w$
76	74 75	coeq12d	$⊢ z = x \to (F (z) L F (w)) \circ (z G w) = (F (x) L F (w)) \circ (x G w)$
77		fveq2	$⊢ w = y \to F (w) = F (y)$
78	77	oveq2d	$⊢ w = y \to F (x) L F (w) = F (x) L F (y)$
79		oveq2	$⊢ w = y \to x G w = x G y$
80	78 79	coeq12d	$⊢ w = y \to (F (x) L F (w)) \circ (x G w) = (F (x) L F (y)) \circ (x G y)$
81		eqid	$⊢ (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) = (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))$
82		ovex	$⊢ F (x) L F (y) \in V$
83		ovex	$⊢ x G y \in V$
84	82 83	coex	$⊢ (F (x) L F (y)) \circ (x G y) \in V$
85	76 80 81 84	ovmpo	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) y = (F (x) L F (y)) \circ (x G y)$
86	85	ad2antlr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) y = (F (x) L F (y)) \circ (x G y)$
87	86	fveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) y) (h) = ((F (x) L F (y)) \circ (x G y)) (h)$
88	87	oveq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (B (U P V) A) (y) (⟨(K \circ F) (x), (K \circ F) (y)⟩ comp (E) (R \circ M) (y)) (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) y) (h) = (B (U P V) A) (y) (⟨(K \circ F) (x), (K \circ F) (y)⟩ comp (E) (R \circ M) (y)) ((F (x) L F (y)) \circ (x G y)) (h)$
89		fveq2	$⊢ z = x \to M (z) = M (x)$
90	89	oveq1d	$⊢ z = x \to M (z) S M (w) = M (x) S M (w)$
91		oveq1	$⊢ z = x \to z N w = x N w$
92	90 91	coeq12d	$⊢ z = x \to (M (z) S M (w)) \circ (z N w) = (M (x) S M (w)) \circ (x N w)$
93		fveq2	$⊢ w = y \to M (w) = M (y)$
94	93	oveq2d	$⊢ w = y \to M (x) S M (w) = M (x) S M (y)$
95		oveq2	$⊢ w = y \to x N w = x N y$
96	94 95	coeq12d	$⊢ w = y \to (M (x) S M (w)) \circ (x N w) = (M (x) S M (y)) \circ (x N y)$
97		eqid	$⊢ (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) = (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))$
98		ovex	$⊢ M (x) S M (y) \in V$
99		ovex	$⊢ x N y \in V$
100	98 99	coex	$⊢ (M (x) S M (y)) \circ (x N y) \in V$
101	92 96 97 100	ovmpo	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) y = (M (x) S M (y)) \circ (x N y)$
102	101	ad2antlr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) y = (M (x) S M (y)) \circ (x N y)$
103	102	fveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) y) (h) = ((M (x) S M (y)) \circ (x N y)) (h)$
104	103	oveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) y) (h) (⟨(K \circ F) (x), (R \circ M) (x)⟩ comp (E) (R \circ M) (y)) (B (U P V) A) (x) = ((M (x) S M (y)) \circ (x N y)) (h) (⟨(K \circ F) (x), (R \circ M) (x)⟩ comp (E) (R \circ M) (y)) (B (U P V) A) (x)$
105	72 88 104	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land h \in (x Hom (C) y)) \to (B (U P V) A) (y) (⟨(K \circ F) (x), (K \circ F) (y)⟩ comp (E) (R \circ M) (y)) (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w)) y) (h) = (x (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w)) y) (h) (⟨(K \circ F) (x), (R \circ M) (x)⟩ comp (E) (R \circ M) (y)) (B (U P V) A) (x)$
106	6 7 8 9 10 19 26 27 63 105	isnatd	$⊢ φ \to B (U P V) A \in (⟨K \circ F, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))⟩ (C Nat E) ⟨R \circ M, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))⟩)$
107	15 22	oveq12d	$⊢ φ \to O (U) (C Nat E) O (V) = ⟨K \circ F, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (F (z) L F (w)) \circ (z G w))⟩ (C Nat E) ⟨R \circ M, (z \in {Base}_{C}, w \in {Base}_{C} ⟼ (M (z) S M (w)) \circ (z N w))⟩$
108	106 107	eleqtrrd	$⊢ φ \to B (U P V) A \in (O (U) (C Nat E) O (V))$

Metamath Proof Explorer

Theorem fuco22natlem

Proof