Theorem parcoval

Description: The composition in the specified parallel-arrow categories is intersection. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	parcoval.m	⊢ 𝑀 = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) )
	parcoval.c	⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ 𝑀 )
	parcoval.s	⊢ 𝑀 ∈ V
	parcoval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
	parcoval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
	parcoval.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	parcoval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
	parcoval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐾 )
Assertion	parcoval	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐺 ∩ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		parcoval.m	⊢ 𝑀 = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) )
2		parcoval.c	⊢ · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ 𝑀 )
3		parcoval.s	⊢ 𝑀 ∈ V
4		parcoval.u	⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
5		parcoval.v	⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
6		parcoval.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
7		parcoval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐾 )
8		parcoval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐾 )
9	2	a1i	⊢ ( 𝜑 → · = ( 𝑝 ∈ ( 𝐵 × 𝐵 ) , 𝑧 ∈ 𝐵 ↦ 𝑀 ) )
10		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑝 = ⟨ 𝑈 , 𝑉 ⟩ ∧ 𝑧 = 𝑊 ) ) → 𝑀 = 𝑀 )
11	4 5	opelxpd	⊢ ( 𝜑 → ⟨ 𝑈 , 𝑉 ⟩ ∈ ( 𝐵 × 𝐵 ) )
12	3	a1i	⊢ ( 𝜑 → 𝑀 ∈ V )
13	9 10 11 6 12	ovmpod	⊢ ( 𝜑 → ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) = 𝑀 )
14	13	oveqd	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐺 𝑀 𝐹 ) )
15	1	a1i	⊢ ( 𝜑 → 𝑀 = ( 𝑓 ∈ 𝐾 , 𝑔 ∈ 𝐾 ↦ ( 𝑓 ∩ 𝑔 ) ) )
16		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → 𝑓 = 𝐺 )
17		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → 𝑔 = 𝐹 )
18	16 17	ineq12d	⊢ ( ( 𝜑 ∧ ( 𝑓 = 𝐺 ∧ 𝑔 = 𝐹 ) ) → ( 𝑓 ∩ 𝑔 ) = ( 𝐺 ∩ 𝐹 ) )
19		inex1g	⊢ ( 𝐺 ∈ 𝐾 → ( 𝐺 ∩ 𝐹 ) ∈ V )
20	8 19	syl	⊢ ( 𝜑 → ( 𝐺 ∩ 𝐹 ) ∈ V )
21	15 18 8 7 20	ovmpod	⊢ ( 𝜑 → ( 𝐺 𝑀 𝐹 ) = ( 𝐺 ∩ 𝐹 ) )
22	14 21	eqtrd	⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑈 , 𝑉 ⟩ · 𝑊 ) 𝐹 ) = ( 𝐺 ∩ 𝐹 ) )