parmapfunc

Description: A map fixing the identity value and preserving the parallel-arrow class induces an endofunctor fixing every object. Category membership and the hom construction suffice: every composable pair contains an identity. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	parmapfunc.b	$⊢ B = {Base}_{C}$
	parmapfunc.h	$⊢ H = Hom (C)$
	parmapfunc.c	$⊢ C \in Cat$
	parmapfunc.hv	$⊢ H = (r \in B, s \in B ⟼ if (r = s, \{J\}, if ((r = X \land s = Y), S, \emptyset)))$
	parmapfunc.l	$⊢ L = (u \in B, v \in B ⟼ (a \in (u H v) ⟼ A (a)))$
	parmapfunc.ai	$⊢ A (J) = J$
	parmapfunc.as	$⊢ \forall t \in S A (t) \in S$
Assertion	parmapfunc	$⊢ ({I ↾}_{B}) (C Func C) L$

Proof

Step	Hyp	Ref	Expression
1		parmapfunc.b	$⊢ B = {Base}_{C}$
2		parmapfunc.h	$⊢ H = Hom (C)$
3		parmapfunc.c	$⊢ C \in Cat$
4		parmapfunc.hv	$⊢ H = (r \in B, s \in B ⟼ if (r = s, \{J\}, if ((r = X \land s = Y), S, \emptyset)))$
5		parmapfunc.l	$⊢ L = (u \in B, v \in B ⟼ (a \in (u H v) ⟼ A (a)))$
6		parmapfunc.ai	$⊢ A (J) = J$
7		parmapfunc.as	$⊢ \forall t \in S A (t) \in S$
8		eqid	$⊢ Id (C) = Id (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10	3	a1i	$⊢ ⊤ \to C \in Cat$
11		f1oi	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B$
12		f1of	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B \to ({I ↾}_{B}) : B ⟶ B$
13	11 12	mp1i	$⊢ ⊤ \to ({I ↾}_{B}) : B ⟶ B$
14	5	fnmpompt	$⊢ L Fn (B \times B)$
15	14	a1i	$⊢ ⊤ \to L Fn (B \times B)$
16		simprl	$⊢ (⊤ \land (x \in B \land y \in B)) \to x \in B$
17		simprr	$⊢ (⊤ \land (x \in B \land y \in B)) \to y \in B$
18	5 16 17	ovmpomptd	$⊢ (⊤ \land (x \in B \land y \in B)) \to x L y = (a \in (x H y) ⟼ A (a))$
19		simpr	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to a \in (x H y)$
20	6	a1i	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to A (J) = J$
21		fveq2	$⊢ t = a \to A (t) = A (a)$
22	21	eleq1d	$⊢ t = a \to (A (t) \in S \leftrightarrow A (a) \in S)$
23	22 7	vtoclri	$⊢ a \in S \to A (a) \in S$
24	23	adantl	$⊢ (((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \land a \in S) \to A (a) \in S$
25	4 19 20 24	parmapcl	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to A (a) \in (x H y)$
26	18 25	fmpt3d	$⊢ (⊤ \land (x \in B \land y \in B)) \to (x L y) : x H y ⟶ x H y$
27		fvresi	$⊢ x \in B \to ({I ↾}_{B}) (x) = x$
28	16 27	syl	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) = x$
29		fvresi	$⊢ y \in B \to ({I ↾}_{B}) (y) = y$
30	17 29	syl	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (y) = y$
31	28 30	oveq12d	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) H ({I ↾}_{B}) (y) = x H y$
32	31	feq3d	$⊢ (⊤ \land (x \in B \land y \in B)) \to ((x L y) : x H y ⟶ ({I ↾}_{B}) (x) H ({I ↾}_{B}) (y) \leftrightarrow (x L y) : x H y ⟶ x H y)$
33	26 32	mpbird	$⊢ (⊤ \land (x \in B \land y \in B)) \to (x L y) : x H y ⟶ ({I ↾}_{B}) (x) H ({I ↾}_{B}) (y)$
34	3	a1i	$⊢ (⊤ \land x \in B) \to C \in Cat$
35		simpr	$⊢ (⊤ \land x \in B) \to x \in B$
36	1 2 4 34 35	paridval	$⊢ (⊤ \land x \in B) \to Id (C) (x) = J$
37	36	fveq2d	$⊢ (⊤ \land x \in B) \to (x L x) (Id (C) (x)) = (x L x) (J)$
38	6	eqcomi	$⊢ J = A (J)$
39	38	fvexi	$⊢ J \in V$
40	4 39 35	parhomid	$⊢ (⊤ \land x \in B) \to J \in (x H x)$
41	5 35 35 40	fvmpomptd	$⊢ (⊤ \land x \in B) \to (x L x) (J) = A (J)$
42	37 41	eqtrd	$⊢ (⊤ \land x \in B) \to (x L x) (Id (C) (x)) = A (J)$
43	27	adantl	$⊢ (⊤ \land x \in B) \to ({I ↾}_{B}) (x) = x$
44	43	fveq2d	$⊢ (⊤ \land x \in B) \to Id (C) (({I ↾}_{B}) (x)) = Id (C) (x)$
45	44 36	eqtrd	$⊢ (⊤ \land x \in B) \to Id (C) (({I ↾}_{B}) (x)) = J$
46	6 42 45	3eqtr4a	$⊢ (⊤ \land x \in B) \to (x L x) (Id (C) (x)) = Id (C) (({I ↾}_{B}) (x))$
47		fvif	$⊢ A (if (x = y, n, m)) = if (x = y, A (n), A (m))$
48	3	a1i	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to C \in Cat$
49		simp3l	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to m \in (x H y)$
50		simp3r	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to n \in (y H z)$
51	1 2 4 48 9 49 50	parcoval2	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to n (⟨x, y⟩ comp (C) z) m = if (x = y, n, m)$
52	51	fveq2d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (x L z) (n (⟨x, y⟩ comp (C) z) m) = (x L z) (if (x = y, n, m))$
53		simp21	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to x \in B$
54		simp23	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to z \in B$
55		simp22	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to y \in B$
56	1 2 9 48 53 55 54 49 50	catcocl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to n (⟨x, y⟩ comp (C) z) m \in (x H z)$
57	51 56	eqeltrrd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to if (x = y, n, m) \in (x H z)$
58	5 53 54 57	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (x L z) (if (x = y, n, m)) = A (if (x = y, n, m))$
59	52 58	eqtrd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (x L z) (n (⟨x, y⟩ comp (C) z) m) = A (if (x = y, n, m))$
60	53 27	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to ({I ↾}_{B}) (x) = x$
61	55 29	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to ({I ↾}_{B}) (y) = y$
62	60 61	opeq12d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to ⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ = ⟨x, y⟩$
63		fvresi	$⊢ z \in B \to ({I ↾}_{B}) (z) = z$
64	54 63	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to ({I ↾}_{B}) (z) = z$
65	62 64	oveq12d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to ⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ comp (C) ({I ↾}_{B}) (z) = ⟨x, y⟩ comp (C) z$
66	5 55 54 50	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (y L z) (n) = A (n)$
67	5 53 55 49	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (x L y) (m) = A (m)$
68	65 66 67	oveq123d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (y L z) (n) (⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ comp (C) ({I ↾}_{B}) (z)) (x L y) (m) = A (n) (⟨x, y⟩ comp (C) z) A (m)$
69	6	a1i	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to A (J) = J$
70		fveq2	$⊢ t = m \to A (t) = A (m)$
71	70	eleq1d	$⊢ t = m \to (A (t) \in S \leftrightarrow A (m) \in S)$
72	71 7	vtoclri	$⊢ m \in S \to A (m) \in S$
73	72	adantl	$⊢ ((⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \land m \in S) \to A (m) \in S$
74	4 49 69 73	parmapcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to A (m) \in (x H y)$
75		fveq2	$⊢ t = n \to A (t) = A (n)$
76	75	eleq1d	$⊢ t = n \to (A (t) \in S \leftrightarrow A (n) \in S)$
77	76 7	vtoclri	$⊢ n \in S \to A (n) \in S$
78	77	adantl	$⊢ ((⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \land n \in S) \to A (n) \in S$
79	4 50 69 78	parmapcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to A (n) \in (y H z)$
80	1 2 4 48 9 74 79	parcoval2	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to A (n) (⟨x, y⟩ comp (C) z) A (m) = if (x = y, A (n), A (m))$
81	68 80	eqtrd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (y L z) (n) (⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ comp (C) ({I ↾}_{B}) (z)) (x L y) (m) = if (x = y, A (n), A (m))$
82	47 59 81	3eqtr4a	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (m \in (x H y) \land n \in (y H z))) \to (x L z) (n (⟨x, y⟩ comp (C) z) m) = (y L z) (n) (⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ comp (C) ({I ↾}_{B}) (z)) (x L y) (m)$
83	1 1 2 2 8 8 9 9 10 10 13 15 33 46 82	isfuncd	$⊢ ⊤ \to ({I ↾}_{B}) (C Func C) L$
84	83	mptru	$⊢ ({I ↾}_{B}) (C Func C) L$

Metamath Proof Explorer

Theorem parmapfunc

Proof