parmapfunc2

Description: Variant of parmapfunc . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

	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$
	parmapfunc2.i	$⊢ I = Id (C)$
	parmapfunc2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
	parmapfunc2.s	$⊢ S \in V$
	parmapfunc2.j	$⊢ J \in V$
	parmapfunc2.p	$⊢ S \subseteq 𝒫 J$
	parmapfunc2.n	$⊢ X \neq Y$
	parmapfunc2.k	$⊢ K = S \cup \{J\}$
	parmapfunc2.mv	$⊢ M = (f \in K, g \in K ⟼ f \cap g)$
	parmapfunc2.ov	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), q \in B ⟼ M)$
	parmapfunc2.iv	$⊢ I = (t \in B ⟼ J)$
Assertion	parmapfunc2	$⊢ ({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		parmapfunc2.i	$⊢ I = Id (C)$
9		parmapfunc2.o	$⊢ \underset{˙}{\cdot} = comp (C)$
10		parmapfunc2.s	$⊢ S \in V$
11		parmapfunc2.j	$⊢ J \in V$
12		parmapfunc2.p	$⊢ S \subseteq 𝒫 J$
13		parmapfunc2.n	$⊢ X \neq Y$
14		parmapfunc2.k	$⊢ K = S \cup \{J\}$
15		parmapfunc2.mv	$⊢ M = (f \in K, g \in K ⟼ f \cap g)$
16		parmapfunc2.ov	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), q \in B ⟼ M)$
17		parmapfunc2.iv	$⊢ I = (t \in B ⟼ J)$
18	3	a1i	$⊢ ⊤ \to C \in Cat$
19		f1oi	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B$
20		f1of	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B \to ({I ↾}_{B}) : B ⟶ B$
21	19 20	mp1i	$⊢ ⊤ \to ({I ↾}_{B}) : B ⟶ B$
22	5	fnmpompt	$⊢ L Fn (B \times B)$
23	22	a1i	$⊢ ⊤ \to L Fn (B \times B)$
24		simprl	$⊢ (⊤ \land (x \in B \land y \in B)) \to x \in B$
25		simprr	$⊢ (⊤ \land (x \in B \land y \in B)) \to y \in B$
26	5 24 25	ovmpomptd	$⊢ (⊤ \land (x \in B \land y \in B)) \to x L y = (a \in (x H y) ⟼ A (a))$
27		simpr	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to a \in (x H y)$
28	6	a1i	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to A (J) = J$
29		fveq2	$⊢ t = a \to A (t) = A (a)$
30	29	eleq1d	$⊢ t = a \to (A (t) \in S \leftrightarrow A (a) \in S)$
31	30 7	vtoclri	$⊢ a \in S \to A (a) \in S$
32	31	adantl	$⊢ (((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \land a \in S) \to A (a) \in S$
33	4 27 28 32	parmapcl	$⊢ ((⊤ \land (x \in B \land y \in B)) \land a \in (x H y)) \to A (a) \in (x H y)$
34	26 33	fmpt3d	$⊢ (⊤ \land (x \in B \land y \in B)) \to (x L y) : x H y ⟶ x H y$
35		fvresi	$⊢ x \in B \to ({I ↾}_{B}) (x) = x$
36	24 35	syl	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) = x$
37		fvresi	$⊢ y \in B \to ({I ↾}_{B}) (y) = y$
38	25 37	syl	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (y) = y$
39	36 38	oveq12d	$⊢ (⊤ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) H ({I ↾}_{B}) (y) = x H y$
40	39	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)$
41	34 40	mpbird	$⊢ (⊤ \land (x \in B \land y \in B)) \to (x L y) : x H y ⟶ ({I ↾}_{B}) (x) H ({I ↾}_{B}) (y)$
42		eqidd	$⊢ ((⊤ \land x \in B) \land t = x) \to J = J$
43		simpr	$⊢ (⊤ \land x \in B) \to x \in B$
44	11	a1i	$⊢ (⊤ \land x \in B) \to J \in V$
45	17 42 43 44	fvmptd2	$⊢ (⊤ \land x \in B) \to I (x) = J$
46	45	fveq2d	$⊢ (⊤ \land x \in B) \to (x L x) (I (x)) = (x L x) (J)$
47	4 11 43	parhomid	$⊢ (⊤ \land x \in B) \to J \in (x H x)$
48	5 43 43 47	fvmpomptd	$⊢ (⊤ \land x \in B) \to (x L x) (J) = A (J)$
49	46 48	eqtrd	$⊢ (⊤ \land x \in B) \to (x L x) (I (x)) = A (J)$
50	35	adantl	$⊢ (⊤ \land x \in B) \to ({I ↾}_{B}) (x) = x$
51	50	fveq2d	$⊢ (⊤ \land x \in B) \to I (({I ↾}_{B}) (x)) = I (x)$
52	51 45	eqtrd	$⊢ (⊤ \land x \in B) \to I (({I ↾}_{B}) (x)) = J$
53	6 49 52	3eqtr4a	$⊢ (⊤ \land x \in B) \to (x L x) (I (x)) = I (({I ↾}_{B}) (x))$
54		snex	$⊢ \{J\} \in V$
55	10 54	unex	$⊢ S \cup \{J\} \in V$
56	14 55	eqeltri	$⊢ K \in V$
57	56 56	mpoex	$⊢ (f \in K, g \in K ⟼ f \cap g) \in V$
58	15 57	eqeltri	$⊢ M \in V$
59		simp21	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to x \in B$
60		simp22	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to y \in B$
61		simp23	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to z \in B$
62		simp3l	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to i \in (x H y)$
63	6	a1i	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (J) = J$
64		fveq2	$⊢ t = i \to A (t) = A (i)$
65	64	eleq1d	$⊢ t = i \to (A (t) \in S \leftrightarrow A (i) \in S)$
66	65 7	vtoclri	$⊢ i \in S \to A (i) \in S$
67	66	adantl	$⊢ ((⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \land i \in S) \to A (i) \in S$
68	4 62 63 67	parmapcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (i) \in (x H y)$
69	4 14 68	parhomcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (i) \in K$
70		simp3r	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to j \in (y H z)$
71		fveq2	$⊢ t = j \to A (t) = A (j)$
72	71	eleq1d	$⊢ t = j \to (A (t) \in S \leftrightarrow A (j) \in S)$
73	72 7	vtoclri	$⊢ j \in S \to A (j) \in S$
74	73	adantl	$⊢ ((⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \land j \in S) \to A (j) \in S$
75	4 70 63 74	parmapcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (j) \in (y H z)$
76	4 14 75	parhomcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (j) \in K$
77	15 16 58 59 60 61 69 76	parcoval	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (j) (⟨x, y⟩ \underset{˙}{\cdot} z) A (i) = A (j) \cap A (i)$
78	59 35	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to ({I ↾}_{B}) (x) = x$
79	60 37	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to ({I ↾}_{B}) (y) = y$
80	78 79	opeq12d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to ⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ = ⟨x, y⟩$
81		fvresi	$⊢ z \in B \to ({I ↾}_{B}) (z) = z$
82	61 81	syl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to ({I ↾}_{B}) (z) = z$
83	80 82	oveq12d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to ⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ \underset{˙}{\cdot} ({I ↾}_{B}) (z) = ⟨x, y⟩ \underset{˙}{\cdot} z$
84	5 60 61 70	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (y L z) (j) = A (j)$
85	5 59 60 62	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L y) (i) = A (i)$
86	83 84 85	oveq123d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (y L z) (j) (⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ \underset{˙}{\cdot} ({I ↾}_{B}) (z)) (x L y) (i) = A (j) (⟨x, y⟩ \underset{˙}{\cdot} z) A (i)$
87	4 14 62	parhomcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to i \in K$
88	4 14 70	parhomcl	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to j \in K$
89	15 16 58 59 60 61 87 88	parcoval	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to j (⟨x, y⟩ \underset{˙}{\cdot} z) i = j \cap i$
90	89	fveq2d	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L z) (j (⟨x, y⟩ \underset{˙}{\cdot} z) i) = (x L z) (j \cap i)$
91	4 62 70 12	parhomco	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to j \cap i \in (x H z)$
92	5 59 61 91	fvmpomptd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L z) (j \cap i) = A (j \cap i)$
93	90 92	eqtrd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L z) (j (⟨x, y⟩ \underset{˙}{\cdot} z) i) = A (j \cap i)$
94	4 12 62 70 63 67 74	parmapco	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to A (j \cap i) = A (j) \cap A (i)$
95	93 94	eqtrd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L z) (j (⟨x, y⟩ \underset{˙}{\cdot} z) i) = A (j) \cap A (i)$
96	77 86 95	3eqtr4rd	$⊢ (⊤ \land (x \in B \land y \in B \land z \in B) \land (i \in (x H y) \land j \in (y H z))) \to (x L z) (j (⟨x, y⟩ \underset{˙}{\cdot} z) i) = (y L z) (j) (⟨({I ↾}_{B}) (x), ({I ↾}_{B}) (y)⟩ \underset{˙}{\cdot} ({I ↾}_{B}) (z)) (x L y) (i)$
97	1 1 2 2 8 8 9 9 18 18 21 23 41 53 96	isfuncd	$⊢ ⊤ \to ({I ↾}_{B}) (C Func C) L$
98	97	mptru	$⊢ ({I ↾}_{B}) (C Func C) L$

Metamath Proof Explorer

Theorem parmapfunc2

Proof