Theorem parhomco

Description: When every member of the parallel-arrow class S is a subset of J , intersection of composable arrows belongs to the hom-set from the first object to the last. The subset hypothesis supplies the required intersection identity laws; it does not follow from the hom construction alone. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
	parhomeqor.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
	parhomeqor.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
	parhomco.p	⊢ 𝑆 ⊆ 𝒫 𝐽
Assertion	parhomco	⊢ ( 𝜑 → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ if ( 𝑥 = 𝑦 , { 𝐽 } , if ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) , 𝑆 , ∅ ) ) )
2		parhomeqor.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
3		parhomeqor.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
4		parhomco.p	⊢ 𝑆 ⊆ 𝒫 𝐽
5	3	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
7		simpr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝑈 = 𝑉 )
8	1 6 7	parhomideq	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐹 = 𝐽 )
9	8	ineq2d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐺 ∩ 𝐽 ) )
10	1 4 3	parhomss	⊢ ( 𝜑 → 𝐺 ⊆ 𝐽 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → 𝐺 ⊆ 𝐽 )
12		dfss2	⊢ ( 𝐺 ⊆ 𝐽 ↔ ( 𝐺 ∩ 𝐽 ) = 𝐺 )
13	11 12	sylib	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐽 ) = 𝐺 )
14	9 13	eqtrd	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) = 𝐺 )
15	7	oveq1d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑈 𝐻 𝑊 ) = ( 𝑉 𝐻 𝑊 ) )
16	5 14 15	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )
17	3	adantr	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 ∈ ( 𝑉 𝐻 𝑊 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝑉 = 𝑊 )
19	1 17 18	parhomideq	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐺 = 𝐽 )
20	19	ineq1d	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = ( 𝐽 ∩ 𝐹 ) )
21	1 4 2	parhomss	⊢ ( 𝜑 → 𝐹 ⊆ 𝐽 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ⊆ 𝐽 )
23		sseqin2	⊢ ( 𝐹 ⊆ 𝐽 ↔ ( 𝐽 ∩ 𝐹 ) = 𝐹 )
24	22 23	sylib	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐽 ∩ 𝐹 ) = 𝐹 )
25	20 24	eqtrd	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) = 𝐹 )
26	2	adantr	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑉 ) )
27	18	oveq2d	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝑈 𝐻 𝑉 ) = ( 𝑈 𝐻 𝑊 ) )
28	26 27	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → 𝐹 ∈ ( 𝑈 𝐻 𝑊 ) )
29	25 28	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑉 = 𝑊 ) → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )
30	1 2 3	parhomeqor	⊢ ( 𝜑 → ( 𝑈 = 𝑉 ∨ 𝑉 = 𝑊 ) )
31	16 29 30	mpjaodan	⊢ ( 𝜑 → ( 𝐺 ∩ 𝐹 ) ∈ ( 𝑈 𝐻 𝑊 ) )