parcoval

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

	Ref	Expression
Hypotheses	parcoval.m	$⊢ M = (f \in K, g \in K ⟼ f \cap g)$
	parcoval.c	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), z \in B ⟼ M)$
	parcoval.s	$⊢ M \in V$
	parcoval.u	$⊢ φ \to U \in B$
	parcoval.v	$⊢ φ \to V \in B$
	parcoval.w	$⊢ φ \to W \in B$
	parcoval.f	$⊢ φ \to F \in K$
	parcoval.g	$⊢ φ \to G \in K$
Assertion	parcoval	$⊢ φ \to G (⟨U, V⟩ \underset{˙}{\cdot} W) F = G \cap F$

Step	Hyp	Ref	Expression
1		parcoval.m	$⊢ M = (f \in K, g \in K ⟼ f \cap g)$
2		parcoval.c	$⊢ \underset{˙}{\cdot} = (p \in (B \times B), z \in B ⟼ M)$
3		parcoval.s	$⊢ M \in V$
4		parcoval.u	$⊢ φ \to U \in B$
5		parcoval.v	$⊢ φ \to V \in B$
6		parcoval.w	$⊢ φ \to W \in B$
7		parcoval.f	$⊢ φ \to F \in K$
8		parcoval.g	$⊢ φ \to G \in K$
9	2	a1i	$⊢ φ \to \underset{˙}{\cdot} = (p \in (B \times B), z \in B ⟼ M)$
10		eqidd	$⊢ (φ \land (p = ⟨U, V⟩ \land z = W)) \to M = M$
11	4 5	opelxpd	$⊢ φ \to ⟨U, V⟩ \in (B \times B)$
12	3	a1i	$⊢ φ \to M \in V$
13	9 10 11 6 12	ovmpod	$⊢ φ \to ⟨U, V⟩ \underset{˙}{\cdot} W = M$
14	13	oveqd	$⊢ φ \to G (⟨U, V⟩ \underset{˙}{\cdot} W) F = G M F$
15	1	a1i	$⊢ φ \to M = (f \in K, g \in K ⟼ f \cap g)$
16		simprl	$⊢ (φ \land (f = G \land g = F)) \to f = G$
17		simprr	$⊢ (φ \land (f = G \land g = F)) \to g = F$
18	16 17	ineq12d	$⊢ (φ \land (f = G \land g = F)) \to f \cap g = G \cap F$
19		inex1g	$⊢ G \in K \to G \cap F \in V$
20	8 19	syl	$⊢ φ \to G \cap F \in V$
21	15 18 8 7 20	ovmpod	$⊢ φ \to G M F = G \cap F$
22	14 21	eqtrd	$⊢ φ \to G (⟨U, V⟩ \underset{˙}{\cdot} W) F = G \cap F$

Metamath Proof Explorer