prcofdiag1

Description: A constant functor pre-composed by a functor is another constant functor. (Contributed by Zhi Wang, 25-Nov-2025)

	Ref	Expression
Hypotheses	prcofdiag.l	$⊢ L = C Δ_{func} D$
	prcofdiag.m	$⊢ M = C Δ_{func} E$
	prcofdiag.f	$⊢ φ \to F \in (E Func D)$
	prcofdiag.c	$⊢ φ \to C \in Cat$
	prcofdiag1.b	$⊢ B = {Base}_{C}$
	prcofdiag1.x	$⊢ φ \to X \in B$
Assertion	prcofdiag1	$⊢ φ \to 1^{st} (L) (X) \circ_{func} F = 1^{st} (M) (X)$

Proof

Step	Hyp	Ref	Expression
1		prcofdiag.l	$⊢ L = C Δ_{func} D$
2		prcofdiag.m	$⊢ M = C Δ_{func} E$
3		prcofdiag.f	$⊢ φ \to F \in (E Func D)$
4		prcofdiag.c	$⊢ φ \to C \in Cat$
5		prcofdiag1.b	$⊢ B = {Base}_{C}$
6		prcofdiag1.x	$⊢ φ \to X \in B$
7		eqid	$⊢ {Base}_{E} = {Base}_{E}$
8	3	func1st2nd	$⊢ φ \to 1^{st} (F) (E Func D) 2^{nd} (F)$
9	8	funcrcl3	$⊢ φ \to D \in Cat$
10		eqid	$⊢ 1^{st} (L) (X) = 1^{st} (L) (X)$
11	1 4 9 5 6 10	diag1cl	$⊢ φ \to 1^{st} (L) (X) \in (D Func C)$
12	3 11	cofucl	$⊢ φ \to 1^{st} (L) (X) \circ_{func} F \in (E Func C)$
13	12	func1st2nd	$⊢ φ \to 1^{st} (1^{st} (L) (X) \circ_{func} F) (E Func C) 2^{nd} (1^{st} (L) (X) \circ_{func} F)$
14	7 5 13	funcf1	$⊢ φ \to 1^{st} (1^{st} (L) (X) \circ_{func} F) : {Base}_{E} ⟶ B$
15	14	ffnd	$⊢ φ \to 1^{st} (1^{st} (L) (X) \circ_{func} F) Fn {Base}_{E}$
16	8	funcrcl2	$⊢ φ \to E \in Cat$
17		eqid	$⊢ 1^{st} (M) (X) = 1^{st} (M) (X)$
18	2 4 16 5 6 17	diag1cl	$⊢ φ \to 1^{st} (M) (X) \in (E Func C)$
19	18	func1st2nd	$⊢ φ \to 1^{st} (1^{st} (M) (X)) (E Func C) 2^{nd} (1^{st} (M) (X))$
20	7 5 19	funcf1	$⊢ φ \to 1^{st} (1^{st} (M) (X)) : {Base}_{E} ⟶ B$
21	20	ffnd	$⊢ φ \to 1^{st} (1^{st} (M) (X)) Fn {Base}_{E}$
22	4	adantr	$⊢ (φ \land x \in {Base}_{E}) \to C \in Cat$
23	9	adantr	$⊢ (φ \land x \in {Base}_{E}) \to D \in Cat$
24	6	adantr	$⊢ (φ \land x \in {Base}_{E}) \to X \in B$
25		eqid	$⊢ {Base}_{D} = {Base}_{D}$
26	7 25 8	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{E} ⟶ {Base}_{D}$
27	26	ffvelcdmda	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (F) (x) \in {Base}_{D}$
28	1 22 23 5 24 10 25 27	diag11	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (1^{st} (L) (X)) (1^{st} (F) (x)) = X$
29	3	adantr	$⊢ (φ \land x \in {Base}_{E}) \to F \in (E Func D)$
30	11	adantr	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (L) (X) \in (D Func C)$
31		simpr	$⊢ (φ \land x \in {Base}_{E}) \to x \in {Base}_{E}$
32	7 29 30 31	cofu1	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (1^{st} (L) (X) \circ_{func} F) (x) = 1^{st} (1^{st} (L) (X)) (1^{st} (F) (x))$
33	16	adantr	$⊢ (φ \land x \in {Base}_{E}) \to E \in Cat$
34	2 22 33 5 24 17 7 31	diag11	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (1^{st} (M) (X)) (x) = X$
35	28 32 34	3eqtr4d	$⊢ (φ \land x \in {Base}_{E}) \to 1^{st} (1^{st} (L) (X) \circ_{func} F) (x) = 1^{st} (1^{st} (M) (X)) (x)$
36	15 21 35	eqfnfvd	$⊢ φ \to 1^{st} (1^{st} (L) (X) \circ_{func} F) = 1^{st} (1^{st} (M) (X))$
37	7 13	funcfn2	$⊢ φ \to 2^{nd} (1^{st} (L) (X) \circ_{func} F) Fn ({Base}_{E} \times {Base}_{E})$
38	7 19	funcfn2	$⊢ φ \to 2^{nd} (1^{st} (M) (X)) Fn ({Base}_{E} \times {Base}_{E})$
39		eqid	$⊢ Hom (E) = Hom (E)$
40		eqid	$⊢ Hom (C) = Hom (C)$
41	13	adantr	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to 1^{st} (1^{st} (L) (X) \circ_{func} F) (E Func C) 2^{nd} (1^{st} (L) (X) \circ_{func} F)$
42		simprl	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to x \in {Base}_{E}$
43		simprr	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to y \in {Base}_{E}$
44	7 39 40 41 42 43	funcf2	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to (x 2^{nd} (1^{st} (L) (X) \circ_{func} F) y) : x Hom (E) y ⟶ 1^{st} (1^{st} (L) (X) \circ_{func} F) (x) Hom (C) 1^{st} (1^{st} (L) (X) \circ_{func} F) (y)$
45	44	ffnd	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to (x 2^{nd} (1^{st} (L) (X) \circ_{func} F) y) Fn (x Hom (E) y)$
46	19	adantr	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to 1^{st} (1^{st} (M) (X)) (E Func C) 2^{nd} (1^{st} (M) (X))$
47	7 39 40 46 42 43	funcf2	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to (x 2^{nd} (1^{st} (M) (X)) y) : x Hom (E) y ⟶ 1^{st} (1^{st} (M) (X)) (x) Hom (C) 1^{st} (1^{st} (M) (X)) (y)$
48	47	ffnd	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to (x 2^{nd} (1^{st} (M) (X)) y) Fn (x Hom (E) y)$
49	4	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to C \in Cat$
50	9	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to D \in Cat$
51	6	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to X \in B$
52	8	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to 1^{st} (F) (E Func D) 2^{nd} (F)$
53	7 25 52	funcf1	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to 1^{st} (F) : {Base}_{E} ⟶ {Base}_{D}$
54	42	adantr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to x \in {Base}_{E}$
55	53 54	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to 1^{st} (F) (x) \in {Base}_{D}$
56		eqid	$⊢ Hom (D) = Hom (D)$
57		eqid	$⊢ Id (C) = Id (C)$
58	43	adantr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to y \in {Base}_{E}$
59	53 58	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to 1^{st} (F) (y) \in {Base}_{D}$
60	7 39 56 52 54 58	funcf2	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (x 2^{nd} (F) y) : x Hom (E) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
61		simpr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to f \in (x Hom (E) y)$
62	60 61	ffvelcdmd	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (x 2^{nd} (F) y) (f) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (y))$
63	1 49 50 5 51 10 25 55 56 57 59 62	diag12	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (1^{st} (F) (x) 2^{nd} (1^{st} (L) (X)) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f)) = Id (C) (X)$
64	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to F \in (E Func D)$
65	11	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to 1^{st} (L) (X) \in (D Func C)$
66	7 64 65 54 58 39 61	cofu2	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (x 2^{nd} (1^{st} (L) (X) \circ_{func} F) y) (f) = (1^{st} (F) (x) 2^{nd} (1^{st} (L) (X)) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
67	16	ad2antrr	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to E \in Cat$
68	2 49 67 5 51 17 7 54 39 57 58 61	diag12	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (x 2^{nd} (1^{st} (M) (X)) y) (f) = Id (C) (X)$
69	63 66 68	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \land f \in (x Hom (E) y)) \to (x 2^{nd} (1^{st} (L) (X) \circ_{func} F) y) (f) = (x 2^{nd} (1^{st} (M) (X)) y) (f)$
70	45 48 69	eqfnfvd	$⊢ (φ \land (x \in {Base}_{E} \land y \in {Base}_{E})) \to x 2^{nd} (1^{st} (L) (X) \circ_{func} F) y = x 2^{nd} (1^{st} (M) (X)) y$
71	37 38 70	eqfnovd	$⊢ φ \to 2^{nd} (1^{st} (L) (X) \circ_{func} F) = 2^{nd} (1^{st} (M) (X))$
72	36 71	opeq12d	$⊢ φ \to ⟨1^{st} (1^{st} (L) (X) \circ_{func} F), 2^{nd} (1^{st} (L) (X) \circ_{func} F)⟩ = ⟨1^{st} (1^{st} (M) (X)), 2^{nd} (1^{st} (M) (X))⟩$
73		relfunc	$⊢ Rel (E Func C)$
74		1st2nd	$⊢ (Rel (E Func C) \land 1^{st} (L) (X) \circ_{func} F \in (E Func C)) \to 1^{st} (L) (X) \circ_{func} F = ⟨1^{st} (1^{st} (L) (X) \circ_{func} F), 2^{nd} (1^{st} (L) (X) \circ_{func} F)⟩$
75	73 12 74	sylancr	$⊢ φ \to 1^{st} (L) (X) \circ_{func} F = ⟨1^{st} (1^{st} (L) (X) \circ_{func} F), 2^{nd} (1^{st} (L) (X) \circ_{func} F)⟩$
76		1st2nd	$⊢ (Rel (E Func C) \land 1^{st} (M) (X) \in (E Func C)) \to 1^{st} (M) (X) = ⟨1^{st} (1^{st} (M) (X)), 2^{nd} (1^{st} (M) (X))⟩$
77	73 18 76	sylancr	$⊢ φ \to 1^{st} (M) (X) = ⟨1^{st} (1^{st} (M) (X)), 2^{nd} (1^{st} (M) (X))⟩$
78	72 75 77	3eqtr4d	$⊢ φ \to 1^{st} (L) (X) \circ_{func} F = 1^{st} (M) (X)$

Metamath Proof Explorer

Theorem prcofdiag1

Proof