prcofdiag

Description: A diagonal functor post-composed by a pre-composition functor is another diagonal 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$
	prcofdiag.g	No typesetting found for \|- ( ph -> ( <. D , C >. -o.F F ) = G ) with typecode \|-
Assertion	prcofdiag	$⊢ φ \to G \circ_{func} L = M$

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		prcofdiag.g	Could not format ( ph -> ( <. D , C >. -o.F F ) = G ) : No typesetting found for \|- ( ph -> ( <. D , C >. -o.F F ) = G ) with typecode \|-
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ {Base}_{(E FuncCat C)} = {Base}_{(E FuncCat C)}$
8	3	func1st2nd	$⊢ φ \to 1^{st} (F) (E Func D) 2^{nd} (F)$
9	8	funcrcl3	$⊢ φ \to D \in Cat$
10		eqid	$⊢ D FuncCat C = D FuncCat C$
11	1 4 9 10	diagcl	$⊢ φ \to L \in (C Func (D FuncCat C))$
12		eqid	$⊢ E FuncCat C = E FuncCat C$
13	10 4 12 3	prcoffunca	Could not format ( ph -> ( <. D , C >. -o.F F ) e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) ) : No typesetting found for \|- ( ph -> ( <. D , C >. -o.F F ) e. ( ( D FuncCat C ) Func ( E FuncCat C ) ) ) with typecode \|-
14	5 13	eqeltrrd	$⊢ φ \to G \in ((D FuncCat C) Func (E FuncCat C))$
15	11 14	cofucl	$⊢ φ \to G \circ_{func} L \in (C Func (E FuncCat C))$
16	15	func1st2nd	$⊢ φ \to 1^{st} (G \circ_{func} L) (C Func (E FuncCat C)) 2^{nd} (G \circ_{func} L)$
17	6 7 16	funcf1	$⊢ φ \to 1^{st} (G \circ_{func} L) : {Base}_{C} ⟶ {Base}_{(E FuncCat C)}$
18	17	ffnd	$⊢ φ \to 1^{st} (G \circ_{func} L) Fn {Base}_{C}$
19	8	funcrcl2	$⊢ φ \to E \in Cat$
20	2 4 19 12	diagcl	$⊢ φ \to M \in (C Func (E FuncCat C))$
21	20	func1st2nd	$⊢ φ \to 1^{st} (M) (C Func (E FuncCat C)) 2^{nd} (M)$
22	6 7 21	funcf1	$⊢ φ \to 1^{st} (M) : {Base}_{C} ⟶ {Base}_{(E FuncCat C)}$
23	22	ffnd	$⊢ φ \to 1^{st} (M) Fn {Base}_{C}$
24	11	adantr	$⊢ (φ \land x \in {Base}_{C}) \to L \in (C Func (D FuncCat C))$
25	14	adantr	$⊢ (φ \land x \in {Base}_{C}) \to G \in ((D FuncCat C) Func (E FuncCat C))$
26		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
27	6 24 25 26	cofu1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G \circ_{func} L) (x) = 1^{st} (G) (1^{st} (L) (x))$
28	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
29	9	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
30		eqid	$⊢ 1^{st} (L) (x) = 1^{st} (L) (x)$
31	1 28 29 6 26 30	diag1cl	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) (x) \in (D Func C)$
32	5	fveq2d	Could not format ( ph -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) ) : No typesetting found for \|- ( ph -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) ) with typecode \|-
33	32	adantr	Could not format ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) ) : No typesetting found for \|- ( ( ph /\ x e. ( Base ` C ) ) -> ( 1st ` ( <. D , C >. -o.F F ) ) = ( 1st ` G ) ) with typecode \|-
34	31 33	prcof1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (1^{st} (L) (x)) = 1^{st} (L) (x) \circ_{func} F$
35	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in (E Func D)$
36	1 2 35 28 6 26	prcofdiag1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (L) (x) \circ_{func} F = 1^{st} (M) (x)$
37	27 34 36	3eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G \circ_{func} L) (x) = 1^{st} (M) (x)$
38	18 23 37	eqfnfvd	$⊢ φ \to 1^{st} (G \circ_{func} L) = 1^{st} (M)$
39	6 16	funcfn2	$⊢ φ \to 2^{nd} (G \circ_{func} L) Fn ({Base}_{C} \times {Base}_{C})$
40	6 21	funcfn2	$⊢ φ \to 2^{nd} (M) Fn ({Base}_{C} \times {Base}_{C})$
41		eqid	$⊢ Hom (C) = Hom (C)$
42		eqid	$⊢ Hom (E FuncCat C) = Hom (E FuncCat C)$
43	16	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} L) (C Func (E FuncCat C)) 2^{nd} (G \circ_{func} L)$
44		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
45		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
46	6 41 42 43 44 45	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (G \circ_{func} L) y) : x Hom (C) y ⟶ 1^{st} (G \circ_{func} L) (x) Hom (E FuncCat C) 1^{st} (G \circ_{func} L) (y)$
47	46	ffnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (G \circ_{func} L) y) Fn (x Hom (C) y)$
48	21	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (M) (C Func (E FuncCat C)) 2^{nd} (M)$
49	6 41 42 48 44 45	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (M) y) : x Hom (C) y ⟶ 1^{st} (M) (x) Hom (E FuncCat C) 1^{st} (M) (y)$
50	49	ffnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (M) y) Fn (x Hom (C) y)$
51		eqid	$⊢ {Base}_{E} = {Base}_{E}$
52		eqid	$⊢ {Base}_{D} = {Base}_{D}$
53	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to F \in (E Func D)$
54	53	func1st2nd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (F) (E Func D) 2^{nd} (F)$
55	51 52 54	funcf1	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (F) : {Base}_{E} ⟶ {Base}_{D}$
56		xpco2	$⊢ 1^{st} (F) : {Base}_{E} ⟶ {Base}_{D} \to ({Base}_{D} \times \{f\}) \circ 1^{st} (F) = {Base}_{E} \times \{f\}$
57	55 56	syl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to ({Base}_{D} \times \{f\}) \circ 1^{st} (F) = {Base}_{E} \times \{f\}$
58	11	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to L \in (C Func (D FuncCat C))$
59	14	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to G \in ((D FuncCat C) Func (E FuncCat C))$
60	44	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to x \in {Base}_{C}$
61	45	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to y \in {Base}_{C}$
62		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to f \in (x Hom (C) y)$
63	6 58 59 60 61 41 62	cofu2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (G \circ_{func} L) y) (f) = (1^{st} (L) (x) 2^{nd} (G) 1^{st} (L) (y)) ((x 2^{nd} (L) y) (f))$
64	4	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to C \in Cat$
65	9	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to D \in Cat$
66	1 6 52 41 64 65 60 61 62	diag2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (L) y) (f) = {Base}_{D} \times \{f\}$
67	66	fveq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (L) (x) 2^{nd} (G) 1^{st} (L) (y)) ((x 2^{nd} (L) y) (f)) = (1^{st} (L) (x) 2^{nd} (G) 1^{st} (L) (y)) ({Base}_{D} \times \{f\})$
68		eqid	$⊢ D Nat C = D Nat C$
69	1 6 52 41 64 65 60 61 62 68	diag2cl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to {Base}_{D} \times \{f\} \in (1^{st} (L) (x) (D Nat C) 1^{st} (L) (y))$
70	5	fveq2d	Could not format ( ph -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) ) : No typesetting found for \|- ( ph -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) ) with typecode \|-
71	70	ad2antrr	Could not format ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) ) : No typesetting found for \|- ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( 2nd ` ( <. D , C >. -o.F F ) ) = ( 2nd ` G ) ) with typecode \|-
72	68 69 71 53	prcof21a	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (L) (x) 2^{nd} (G) 1^{st} (L) (y)) ({Base}_{D} \times \{f\}) = ({Base}_{D} \times \{f\}) \circ 1^{st} (F)$
73	63 67 72	3eqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (G \circ_{func} L) y) (f) = ({Base}_{D} \times \{f\}) \circ 1^{st} (F)$
74	19	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to E \in Cat$
75	2 6 51 41 64 74 60 61 62	diag2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (M) y) (f) = {Base}_{E} \times \{f\}$
76	57 73 75	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (G \circ_{func} L) y) (f) = (x 2^{nd} (M) y) (f)$
77	47 50 76	eqfnfvd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G \circ_{func} L) y = x 2^{nd} (M) y$
78	39 40 77	eqfnovd	$⊢ φ \to 2^{nd} (G \circ_{func} L) = 2^{nd} (M)$
79	38 78	opeq12d	$⊢ φ \to ⟨1^{st} (G \circ_{func} L), 2^{nd} (G \circ_{func} L)⟩ = ⟨1^{st} (M), 2^{nd} (M)⟩$
80		relfunc	$⊢ Rel (C Func (E FuncCat C))$
81		1st2nd	$⊢ (Rel (C Func (E FuncCat C)) \land G \circ_{func} L \in (C Func (E FuncCat C))) \to G \circ_{func} L = ⟨1^{st} (G \circ_{func} L), 2^{nd} (G \circ_{func} L)⟩$
82	80 15 81	sylancr	$⊢ φ \to G \circ_{func} L = ⟨1^{st} (G \circ_{func} L), 2^{nd} (G \circ_{func} L)⟩$
83		1st2nd	$⊢ (Rel (C Func (E FuncCat C)) \land M \in (C Func (E FuncCat C))) \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
84	80 20 83	sylancr	$⊢ φ \to M = ⟨1^{st} (M), 2^{nd} (M)⟩$
85	79 82 84	3eqtr4d	$⊢ φ \to G \circ_{func} L = M$

Metamath Proof Explorer

Theorem prcofdiag

Proof