parcatid2

Description: Variant of parcatid . (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	parcatid.b	$⊢ B \in V$
	parcatid.j	$⊢ J \in V$
	parcatid.p	$⊢ S \subseteq 𝒫 J$
	parcatid.k	$⊢ K = S \cup \{J\}$
	parcatid.h	$⊢ H = (m \in B, n \in B ⟼ if (m = n, \{J\}, if ((m = X \land n = Y), S, \emptyset)))$
	parcatid.m	$⊢ M = (r \in K, s \in K ⟼ r \cap s)$
	parcatid.o	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), q \in B ⟼ M)$
	parcatid.c	$⊢ C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
	parcatid2.s	$⊢ S \in V$
	parcatid2.n	$⊢ X \neq Y$
Assertion	parcatid2	$⊢ (C \in Cat \land Id (C) = (y \in B ⟼ J))$

Proof

Step	Hyp	Ref	Expression
1		parcatid.b	$⊢ B \in V$
2		parcatid.j	$⊢ J \in V$
3		parcatid.p	$⊢ S \subseteq 𝒫 J$
4		parcatid.k	$⊢ K = S \cup \{J\}$
5		parcatid.h	$⊢ H = (m \in B, n \in B ⟼ if (m = n, \{J\}, if ((m = X \land n = Y), S, \emptyset)))$
6		parcatid.m	$⊢ M = (r \in K, s \in K ⟼ r \cap s)$
7		parcatid.o	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), q \in B ⟼ M)$
8		parcatid.c	$⊢ C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
9		parcatid2.s	$⊢ S \in V$
10		parcatid2.n	$⊢ X \neq Y$
11	8 1	catbas	$⊢ B = {Base}_{C}$
12	11	a1i	$⊢ ⊤ \to B = {Base}_{C}$
13	1 1	mpoex	$⊢ (m \in B, n \in B ⟼ if (m = n, \{J\}, if ((m = X \land n = Y), S, \emptyset))) \in V$
14	5 13	eqeltri	$⊢ H \in V$
15	8 14	cathomfval	$⊢ H = Hom (C)$
16	15	a1i	$⊢ ⊤ \to H = Hom (C)$
17	1 1	xpex	$⊢ B \times B \in V$
18	17 1	mpoex	$⊢ (p \in (B \times B), q \in B ⟼ M) \in V$
19	7 18	eqeltri	$⊢ \underset{˙}{\cdot} \in V$
20	8 19	catcofval	$⊢ \underset{˙}{\cdot} = comp (C)$
21	20	a1i	$⊢ ⊤ \to \underset{˙}{\cdot} = comp (C)$
22		tpex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\} \in V$
23	8 22	eqeltri	$⊢ C \in V$
24	23	a1i	$⊢ ⊤ \to C \in V$
25		biid	$⊢ ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w))) \leftrightarrow ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
26		simpr	$⊢ (⊤ \land y \in B) \to y \in B$
27	5 2 26	parhomid	$⊢ (⊤ \land y \in B) \to J \in (y H y)$
28		snex	$⊢ \{J\} \in V$
29	9 28	unex	$⊢ S \cup \{J\} \in V$
30	4 29	eqeltri	$⊢ K \in V$
31	30 30	mpoex	$⊢ (r \in K, s \in K ⟼ r \cap s) \in V$
32	6 31	eqeltri	$⊢ M \in V$
33		simpr	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))$
34	33	simp1d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (x \in B \land y \in B)$
35	34	simpld	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to x \in B$
36	34	simprd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to y \in B$
37	33	simp3d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (f \in (x H y) \land g \in (y H z) \land k \in (z H w))$
38	37	simp1d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to f \in (x H y)$
39	5 4 38	parhomcl	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to f \in K$
40	2	snid	$⊢ J \in \{J\}$
41		elun2	$⊢ J \in \{J\} \to J \in (S \cup \{J\})$
42	40 41	ax-mp	$⊢ J \in (S \cup \{J\})$
43	42 4	eleqtrri	$⊢ J \in K$
44	43	a1i	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to J \in K$
45	6 7 32 35 36 36 39 44	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to J (⟨x, y⟩ \underset{˙}{\cdot} y) f = J \cap f$
46	5 3 38	parhomss	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to f \subseteq J$
47		sseqin2	$⊢ f \subseteq J \leftrightarrow J \cap f = f$
48	46 47	sylib	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to J \cap f = f$
49	45 48	eqtrd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to J (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
50	33	simp2d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (z \in B \land w \in B)$
51	50	simpld	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to z \in B$
52	37	simp2d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \in (y H z)$
53	5 4 52	parhomcl	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \in K$
54	6 7 32 36 36 51 44 53	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) J = g \cap J$
55	5 3 52	parhomss	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \subseteq J$
56		dfss2	$⊢ g \subseteq J \leftrightarrow g \cap J = g$
57	55 56	sylib	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \cap J = g$
58	54 57	eqtrd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) J = g$
59	6 7 32 35 36 51 39 53	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f = g \cap f$
60	5 38 52 3	parhomco	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \cap f \in (x H z)$
61	59 60	eqeltrd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x H z)$
62		inass	$⊢ (k \cap g) \cap f = k \cap (g \cap f)$
63	50	simprd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to w \in B$
64	37	simp3d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k \in (z H w)$
65	5 4 64	parhomcl	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k \in K$
66	6 7 32 36 51 63 53 65	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨y, z⟩ \underset{˙}{\cdot} w) g = k \cap g$
67	66	oveq1d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k \cap g) (⟨x, y⟩ \underset{˙}{\cdot} w) f$
68	5 52 64 3	parhomco	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k \cap g \in (y H w)$
69	5 4 68	parhomcl	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k \cap g \in K$
70	6 7 32 35 36 63 39 69	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k \cap g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k \cap g) \cap f$
71	67 70	eqtrd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = (k \cap g) \cap f$
72	59	oveq2d	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g \cap f)$
73	5 4 60	parhomcl	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to g \cap f \in K$
74	6 7 32 35 51 63 73 65	parcoval	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g \cap f) = k \cap (g \cap f)$
75	72 74	eqtrd	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f) = k \cap (g \cap f)$
76	62 71 75	3eqtr4a	$⊢ (⊤ \land ((x \in B \land y \in B) \land (z \in B \land w \in B) \land (f \in (x H y) \land g \in (y H z) \land k \in (z H w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
77	12 16 21 24 25 27 49 58 61 76	iscatd2	$⊢ ⊤ \to (C \in Cat \land Id (C) = (y \in B ⟼ J))$
78	77	mptru	$⊢ (C \in Cat \land Id (C) = (y \in B ⟼ J))$

Metamath Proof Explorer

Theorem parcatid2

Proof