Theorem 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	⊢ 𝐵 ∈ V
	parcatid.j	⊢ 𝐽 ∈ V
	parcatid.p	⊢ 𝑆 ⊆ 𝒫 𝐽
	parcatid.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
	parcatid.h	⊢ 𝐻 = ( 𝑚 ∈ 𝐵 , 𝑛 ∈ 𝐵 ↦ if ( 𝑚 = 𝑛 , { 𝐽 } , if ( ( 𝑚 = 𝑋 ∧ 𝑛 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parcatid.m	⊢ 𝑀 = ( 𝑟 ∈ 𝐾 , 𝑠 ∈ 𝐾 ↦ ( 𝑟 ∩ 𝑠 ) )
	parcatid.o	⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑞 ∈ 𝐵 ↦ 𝑀 )
	parcatid.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ }
	parcatid2.s	⊢ 𝑆 ∈ V
	parcatid2.n	⊢ 𝑋 ≠ 𝑌
Assertion	parcatid2	⊢ ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		parcatid.b	⊢ 𝐵 ∈ V
2		parcatid.j	⊢ 𝐽 ∈ V
3		parcatid.p	⊢ 𝑆 ⊆ 𝒫 𝐽
4		parcatid.k	⊢ 𝐾 = ( 𝑆 ∪ { 𝐽 } )
5		parcatid.h	⊢ 𝐻 = ( 𝑚 ∈ 𝐵 , 𝑛 ∈ 𝐵 ↦ if ( 𝑚 = 𝑛 , { 𝐽 } , if ( ( 𝑚 = 𝑋 ∧ 𝑛 = 𝑌 ) , 𝑆 , ∅ ) ) )
6		parcatid.m	⊢ 𝑀 = ( 𝑟 ∈ 𝐾 , 𝑠 ∈ 𝐾 ↦ ( 𝑟 ∩ 𝑠 ) )
7		parcatid.o	⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑞 ∈ 𝐵 ↦ 𝑀 )
8		parcatid.c	⊢ 𝐶 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ }
9		parcatid2.s	⊢ 𝑆 ∈ V
10		parcatid2.n	⊢ 𝑋 ≠ 𝑌
11	8 1	catbas	⊢ 𝐵 = ( Base ‘ 𝐶 )
12	11	a1i	⊢ ( ⊤ → 𝐵 = ( Base ‘ 𝐶 ) )
13	1 1	mpoex	⊢ ( 𝑚 ∈ 𝐵 , 𝑛 ∈ 𝐵 ↦ if ( 𝑚 = 𝑛 , { 𝐽 } , if ( ( 𝑚 = 𝑋 ∧ 𝑛 = 𝑌 ) , 𝑆 , ∅ ) ) ) ∈ V
14	5 13	eqeltri	⊢ 𝐻 ∈ V
15	8 14	cathomfval	⊢ 𝐻 = ( Hom ‘ 𝐶 )
16	15	a1i	⊢ ( ⊤ → 𝐻 = ( Hom ‘ 𝐶 ) )
17	1 1	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
18	17 1	mpoex	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑞 ∈ 𝐵 ↦ 𝑀 ) ∈ V
19	7 18	eqeltri	⊢ · ∈ V
20	8 19	catcofval	⊢ · = ( comp ‘ 𝐶 )
21	20	a1i	⊢ ( ⊤ → · = ( comp ‘ 𝐶 ) )
22		tpex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ , ⟨ ( comp ‘ ndx ) , · ⟩ } ∈ V
23	8 22	eqeltri	⊢ 𝐶 ∈ V
24	23	a1i	⊢ ( ⊤ → 𝐶 ∈ V )
25		biid	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
26		simpr	⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
27	5 2 26	parhomid	⊢ ( ( ⊤ ∧ 𝑦 ∈ 𝐵 ) → 𝐽 ∈ ( 𝑦 𝐻 𝑦 ) )
28		snex	⊢ { 𝐽 } ∈ V
29	9 28	unex	⊢ ( 𝑆 ∪ { 𝐽 } ) ∈ V
30	4 29	eqeltri	⊢ 𝐾 ∈ V
31	30 30	mpoex	⊢ ( 𝑟 ∈ 𝐾 , 𝑠 ∈ 𝐾 ↦ ( 𝑟 ∩ 𝑠 ) ) ∈ V
32	6 31	eqeltri	⊢ 𝑀 ∈ V
33		simpr	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) )
34	33	simp1d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
35	34	simpld	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑥 ∈ 𝐵 )
36	34	simprd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑦 ∈ 𝐵 )
37	33	simp3d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) )
38	37	simp1d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
39	5 4 38	parhomcl	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑓 ∈ 𝐾 )
40	2	snid	⊢ 𝐽 ∈ { 𝐽 }
41		elun2	⊢ ( 𝐽 ∈ { 𝐽 } → 𝐽 ∈ ( 𝑆 ∪ { 𝐽 } ) )
42	40 41	ax-mp	⊢ 𝐽 ∈ ( 𝑆 ∪ { 𝐽 } )
43	42 4	eleqtrri	⊢ 𝐽 ∈ 𝐾
44	43	a1i	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝐽 ∈ 𝐾 )
45	6 7 32 35 36 36 39 44	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝐽 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = ( 𝐽 ∩ 𝑓 ) )
46	5 3 38	parhomss	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑓 ⊆ 𝐽 )
47		sseqin2	⊢ ( 𝑓 ⊆ 𝐽 ↔ ( 𝐽 ∩ 𝑓 ) = 𝑓 )
48	46 47	sylib	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝐽 ∩ 𝑓 ) = 𝑓 )
49	45 48	eqtrd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝐽 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑦 ) 𝑓 ) = 𝑓 )
50	33	simp2d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) )
51	50	simpld	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑧 ∈ 𝐵 )
52	37	simp2d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) )
53	5 4 52	parhomcl	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑔 ∈ 𝐾 )
54	6 7 32 36 36 51 44 53	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 𝐽 ) = ( 𝑔 ∩ 𝐽 ) )
55	5 3 52	parhomss	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑔 ⊆ 𝐽 )
56		dfss2	⊢ ( 𝑔 ⊆ 𝐽 ↔ ( 𝑔 ∩ 𝐽 ) = 𝑔 )
57	55 56	sylib	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ∩ 𝐽 ) = 𝑔 )
58	54 57	eqtrd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑦 , 𝑦 ⟩ · 𝑧 ) 𝐽 ) = 𝑔 )
59	6 7 32 35 36 51 39 53	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) = ( 𝑔 ∩ 𝑓 ) )
60	5 38 52 3	parhomco	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ∩ 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
61	59 60	eqeltrd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐻 𝑧 ) )
62		inass	⊢ ( ( 𝑘 ∩ 𝑔 ) ∩ 𝑓 ) = ( 𝑘 ∩ ( 𝑔 ∩ 𝑓 ) )
63	50	simprd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑤 ∈ 𝐵 )
64	37	simp3d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) )
65	5 4 64	parhomcl	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → 𝑘 ∈ 𝐾 )
66	6 7 32 36 51 63 53 65	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) = ( 𝑘 ∩ 𝑔 ) )
67	66	oveq1d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ∩ 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) )
68	5 52 64 3	parhomco	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ∩ 𝑔 ) ∈ ( 𝑦 𝐻 𝑤 ) )
69	5 4 68	parhomcl	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ∩ 𝑔 ) ∈ 𝐾 )
70	6 7 32 35 36 63 39 69	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ∩ 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ∩ 𝑔 ) ∩ 𝑓 ) )
71	67 70	eqtrd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( ( 𝑘 ∩ 𝑔 ) ∩ 𝑓 ) )
72	59	oveq2d	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ∩ 𝑓 ) ) )
73	5 4 60	parhomcl	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑔 ∩ 𝑓 ) ∈ 𝐾 )
74	6 7 32 35 51 63 73 65	parcoval	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ∩ 𝑓 ) ) = ( 𝑘 ∩ ( 𝑔 ∩ 𝑓 ) ) )
75	72 74	eqtrd	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) = ( 𝑘 ∩ ( 𝑔 ∩ 𝑓 ) ) )
76	62 71 75	3eqtr4a	⊢ ( ( ⊤ ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 𝐻 𝑧 ) ∧ 𝑘 ∈ ( 𝑧 𝐻 𝑤 ) ) ) ) → ( ( 𝑘 ( ⟨ 𝑦 , 𝑧 ⟩ · 𝑤 ) 𝑔 ) ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑤 ) 𝑓 ) = ( 𝑘 ( ⟨ 𝑥 , 𝑧 ⟩ · 𝑤 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ) )
77	12 16 21 24 25 27 49 58 61 76	iscatd2	⊢ ( ⊤ → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐽 ) ) )
78	77	mptru	⊢ ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐽 ) )