fucoid

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid2 . (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fucoid.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fucoid.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
	fucoid.1	$⊢ \underset{˙}{1} = Id (T)$
	fucoid.q	$⊢ Q = C FuncCat E$
	fucoid.i	$⊢ I = Id (Q)$
	fucoid.f	$⊢ φ \to F (C Func D) G$
	fucoid.k	$⊢ φ \to K (D Func E) L$
	fucoid.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
Assertion	fucoid	$⊢ φ \to (U P U) (\underset{˙}{1} (U)) = I (O (U))$

Proof

Step	Hyp	Ref	Expression
1		fucoid.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		fucoid.t	$⊢ T = (D FuncCat E) \times_{c} (C FuncCat D)$
3		fucoid.1	$⊢ \underset{˙}{1} = Id (T)$
4		fucoid.q	$⊢ Q = C FuncCat E$
5		fucoid.i	$⊢ I = Id (Q)$
6		fucoid.f	$⊢ φ \to F (C Func D) G$
7		fucoid.k	$⊢ φ \to K (D Func E) L$
8		fucoid.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
9		ovex	$⊢ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x)) \in V$
10		eqid	$⊢ (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) = (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x)))$
11	9 10	fnmpti	$⊢ (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) Fn {Base}_{C}$
12	11	a1i	$⊢ φ \to (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) Fn {Base}_{C}$
13	7	funcrcl3	$⊢ φ \to E \in Cat$
14		eqid	$⊢ {Base}_{E} = {Base}_{E}$
15		eqid	$⊢ Id (E) = Id (E)$
16	14 15	cidfn	$⊢ E \in Cat \to Id (E) Fn {Base}_{E}$
17	13 16	syl	$⊢ φ \to Id (E) Fn {Base}_{E}$
18		eqid	$⊢ {Base}_{D} = {Base}_{D}$
19	18 14 7	funcf1	$⊢ φ \to K : {Base}_{D} ⟶ {Base}_{E}$
20		eqid	$⊢ {Base}_{C} = {Base}_{C}$
21	20 18 6	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
22	19 21	fcod	$⊢ φ \to (K \circ F) : {Base}_{C} ⟶ {Base}_{E}$
23		fnfco	$⊢ (Id (E) Fn {Base}_{E} \land (K \circ F) : {Base}_{C} ⟶ {Base}_{E}) \to (Id (E) \circ (K \circ F)) Fn {Base}_{C}$
24	17 22 23	syl2anc	$⊢ φ \to (Id (E) \circ (K \circ F)) Fn {Base}_{C}$
25		2fveq3	$⊢ x = w \to K (F (x)) = K (F (w))$
26	25 25	opeq12d	$⊢ x = w \to ⟨K (F (x)), K (F (x))⟩ = ⟨K (F (w)), K (F (w))⟩$
27	26 25	oveq12d	$⊢ x = w \to ⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x)) = ⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))$
28		2fveq3	$⊢ x = w \to (Id (E) \circ K) (F (x)) = (Id (E) \circ K) (F (w))$
29		fveq2	$⊢ x = w \to F (x) = F (w)$
30	29 29	oveq12d	$⊢ x = w \to F (x) L F (x) = F (w) L F (w)$
31		fveq2	$⊢ x = w \to (Id (D) \circ F) (x) = (Id (D) \circ F) (w)$
32	30 31	fveq12d	$⊢ x = w \to (F (x) L F (x)) ((Id (D) \circ F) (x)) = (F (w) L F (w)) ((Id (D) \circ F) (w))$
33	27 28 32	oveq123d	$⊢ x = w \to (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x)) = (Id (E) \circ K) (F (w)) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) (F (w) L F (w)) ((Id (D) \circ F) (w))$
34		simpr	$⊢ (φ \land w \in {Base}_{C}) \to w \in {Base}_{C}$
35		ovexd	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ K) (F (w)) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) (F (w) L F (w)) ((Id (D) \circ F) (w)) \in V$
36	10 33 34 35	fvmptd3	$⊢ (φ \land w \in {Base}_{C}) \to (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) (w) = (Id (E) \circ K) (F (w)) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) (F (w) L F (w)) ((Id (D) \circ F) (w))$
37		eqid	$⊢ Hom (E) = Hom (E)$
38	13	adantr	$⊢ (φ \land w \in {Base}_{C}) \to E \in Cat$
39	19	adantr	$⊢ (φ \land w \in {Base}_{C}) \to K : {Base}_{D} ⟶ {Base}_{E}$
40	21	ffvelcdmda	$⊢ (φ \land w \in {Base}_{C}) \to F (w) \in {Base}_{D}$
41	39 40	ffvelcdmd	$⊢ (φ \land w \in {Base}_{C}) \to K (F (w)) \in {Base}_{E}$
42		eqid	$⊢ comp (E) = comp (E)$
43	14 37 15 38 41	catidcl	$⊢ (φ \land w \in {Base}_{C}) \to Id (E) (K (F (w))) \in (K (F (w)) Hom (E) K (F (w)))$
44	14 37 15 38 41 42 41 43	catlid	$⊢ (φ \land w \in {Base}_{C}) \to Id (E) (K (F (w))) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) Id (E) (K (F (w))) = Id (E) (K (F (w)))$
45	39 40	fvco3d	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ K) (F (w)) = Id (E) (K (F (w)))$
46	21	adantr	$⊢ (φ \land w \in {Base}_{C}) \to F : {Base}_{C} ⟶ {Base}_{D}$
47	46 34	fvco3d	$⊢ (φ \land w \in {Base}_{C}) \to (Id (D) \circ F) (w) = Id (D) (F (w))$
48	47	fveq2d	$⊢ (φ \land w \in {Base}_{C}) \to (F (w) L F (w)) ((Id (D) \circ F) (w)) = (F (w) L F (w)) (Id (D) (F (w)))$
49		eqid	$⊢ Id (D) = Id (D)$
50	7	adantr	$⊢ (φ \land w \in {Base}_{C}) \to K (D Func E) L$
51	18 49 15 50 40	funcid	$⊢ (φ \land w \in {Base}_{C}) \to (F (w) L F (w)) (Id (D) (F (w))) = Id (E) (K (F (w)))$
52	48 51	eqtrd	$⊢ (φ \land w \in {Base}_{C}) \to (F (w) L F (w)) ((Id (D) \circ F) (w)) = Id (E) (K (F (w)))$
53	45 52	oveq12d	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ K) (F (w)) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) (F (w) L F (w)) ((Id (D) \circ F) (w)) = Id (E) (K (F (w))) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) Id (E) (K (F (w)))$
54	22	adantr	$⊢ (φ \land w \in {Base}_{C}) \to (K \circ F) : {Base}_{C} ⟶ {Base}_{E}$
55	54 34	fvco3d	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ (K \circ F)) (w) = Id (E) ((K \circ F) (w))$
56	46 34	fvco3d	$⊢ (φ \land w \in {Base}_{C}) \to (K \circ F) (w) = K (F (w))$
57	56	fveq2d	$⊢ (φ \land w \in {Base}_{C}) \to Id (E) ((K \circ F) (w)) = Id (E) (K (F (w)))$
58	55 57	eqtrd	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ (K \circ F)) (w) = Id (E) (K (F (w)))$
59	44 53 58	3eqtr4d	$⊢ (φ \land w \in {Base}_{C}) \to (Id (E) \circ K) (F (w)) (⟨K (F (w)), K (F (w))⟩ comp (E) K (F (w))) (F (w) L F (w)) ((Id (D) \circ F) (w)) = (Id (E) \circ (K \circ F)) (w)$
60	36 59	eqtrd	$⊢ (φ \land w \in {Base}_{C}) \to (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) (w) = (Id (E) \circ (K \circ F)) (w)$
61	12 24 60	eqfnfvd	$⊢ φ \to (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x))) = Id (E) \circ (K \circ F)$
62	8	fveq2d	$⊢ φ \to \underset{˙}{1} (U) = \underset{˙}{1} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
63		eqid	$⊢ D FuncCat E = D FuncCat E$
64	7	funcrcl2	$⊢ φ \to D \in Cat$
65	63 64 13	fuccat	$⊢ φ \to D FuncCat E \in Cat$
66		eqid	$⊢ C FuncCat D = C FuncCat D$
67	6	funcrcl2	$⊢ φ \to C \in Cat$
68	66 67 64	fuccat	$⊢ φ \to C FuncCat D \in Cat$
69	63	fucbas	$⊢ D Func E = {Base}_{(D FuncCat E)}$
70	66	fucbas	$⊢ C Func D = {Base}_{(C FuncCat D)}$
71		eqid	$⊢ Id (D FuncCat E) = Id (D FuncCat E)$
72		eqid	$⊢ Id (C FuncCat D) = Id (C FuncCat D)$
73		df-br	$⊢ K (D Func E) L \leftrightarrow ⟨K, L⟩ \in (D Func E)$
74	7 73	sylib	$⊢ φ \to ⟨K, L⟩ \in (D Func E)$
75		df-br	$⊢ F (C Func D) G \leftrightarrow ⟨F, G⟩ \in (C Func D)$
76	6 75	sylib	$⊢ φ \to ⟨F, G⟩ \in (C Func D)$
77	2 65 68 69 70 71 72 3 74 76	xpcid	$⊢ φ \to \underset{˙}{1} (⟨⟨K, L⟩, ⟨F, G⟩⟩) = ⟨Id (D FuncCat E) (⟨K, L⟩), Id (C FuncCat D) (⟨F, G⟩)⟩$
78	63 71 15 74	fucid	$⊢ φ \to Id (D FuncCat E) (⟨K, L⟩) = Id (E) \circ 1^{st} (⟨K, L⟩)$
79		relfunc	$⊢ Rel (D Func E)$
80	79	brrelex1i	$⊢ K (D Func E) L \to K \in V$
81	7 80	syl	$⊢ φ \to K \in V$
82	79	brrelex2i	$⊢ K (D Func E) L \to L \in V$
83	7 82	syl	$⊢ φ \to L \in V$
84		op1stg	$⊢ (K \in V \land L \in V) \to 1^{st} (⟨K, L⟩) = K$
85	81 83 84	syl2anc	$⊢ φ \to 1^{st} (⟨K, L⟩) = K$
86	85	coeq2d	$⊢ φ \to Id (E) \circ 1^{st} (⟨K, L⟩) = Id (E) \circ K$
87	78 86	eqtrd	$⊢ φ \to Id (D FuncCat E) (⟨K, L⟩) = Id (E) \circ K$
88	66 72 49 76	fucid	$⊢ φ \to Id (C FuncCat D) (⟨F, G⟩) = Id (D) \circ 1^{st} (⟨F, G⟩)$
89		relfunc	$⊢ Rel (C Func D)$
90	89	brrelex1i	$⊢ F (C Func D) G \to F \in V$
91	6 90	syl	$⊢ φ \to F \in V$
92	89	brrelex2i	$⊢ F (C Func D) G \to G \in V$
93	6 92	syl	$⊢ φ \to G \in V$
94		op1stg	$⊢ (F \in V \land G \in V) \to 1^{st} (⟨F, G⟩) = F$
95	91 93 94	syl2anc	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
96	95	coeq2d	$⊢ φ \to Id (D) \circ 1^{st} (⟨F, G⟩) = Id (D) \circ F$
97	88 96	eqtrd	$⊢ φ \to Id (C FuncCat D) (⟨F, G⟩) = Id (D) \circ F$
98	87 97	opeq12d	$⊢ φ \to ⟨Id (D FuncCat E) (⟨K, L⟩), Id (C FuncCat D) (⟨F, G⟩)⟩ = ⟨Id (E) \circ K, Id (D) \circ F⟩$
99	62 77 98	3eqtrd	$⊢ φ \to \underset{˙}{1} (U) = ⟨Id (E) \circ K, Id (D) \circ F⟩$
100	99	fveq2d	$⊢ φ \to (U P U) (\underset{˙}{1} (U)) = (U P U) (⟨Id (E) \circ K, Id (D) \circ F⟩)$
101		df-ov	$⊢ (Id (E) \circ K) (U P U) (Id (D) \circ F) = (U P U) (⟨Id (E) \circ K, Id (D) \circ F⟩)$
102	100 101	eqtr4di	$⊢ φ \to (U P U) (\underset{˙}{1} (U)) = (Id (E) \circ K) (U P U) (Id (D) \circ F)$
103		eqid	$⊢ C Nat D = C Nat D$
104	66 103	fuchom	$⊢ C Nat D = Hom (C FuncCat D)$
105	70 104 72 68 76	catidcl	$⊢ φ \to Id (C FuncCat D) (⟨F, G⟩) \in (⟨F, G⟩ (C Nat D) ⟨F, G⟩)$
106	97 105	eqeltrrd	$⊢ φ \to Id (D) \circ F \in (⟨F, G⟩ (C Nat D) ⟨F, G⟩)$
107		eqid	$⊢ D Nat E = D Nat E$
108	63 107	fuchom	$⊢ D Nat E = Hom (D FuncCat E)$
109	69 108 71 65 74	catidcl	$⊢ φ \to Id (D FuncCat E) (⟨K, L⟩) \in (⟨K, L⟩ (D Nat E) ⟨K, L⟩)$
110	87 109	eqeltrrd	$⊢ φ \to Id (E) \circ K \in (⟨K, L⟩ (D Nat E) ⟨K, L⟩)$
111	1 8 8 106 110	fuco22	$⊢ φ \to (Id (E) \circ K) (U P U) (Id (D) \circ F) = (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x)))$
112	102 111	eqtrd	$⊢ φ \to (U P U) (\underset{˙}{1} (U)) = (x \in {Base}_{C} ⟼ (Id (E) \circ K) (F (x)) (⟨K (F (x)), K (F (x))⟩ comp (E) K (F (x))) (F (x) L F (x)) ((Id (D) \circ F) (x)))$
113	1 6 7 8 4 5 15	fuco11id	$⊢ φ \to I (O (U)) = Id (E) \circ (K \circ F)$
114	61 112 113	3eqtr4d	$⊢ φ \to (U P U) (\underset{˙}{1} (U)) = I (O (U))$

Metamath Proof Explorer

Theorem fucoid

Proof