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	|- M = ( f e. K , g e. K |-> ( f i^i g ) )
	parcoval.c	|- .x. = ( p e. ( B X. B ) , z e. B |-> M )
	parcoval.s	|- M e. _V
	parcoval.u	|- ( ph -> U e. B )
	parcoval.v	|- ( ph -> V e. B )
	parcoval.w	|- ( ph -> W e. B )
	parcoval.f	|- ( ph -> F e. K )
	parcoval.g	|- ( ph -> G e. K )
Assertion	parcoval	|- ( ph -> ( G ( <. U , V >. .x. W ) F ) = ( G i^i F ) )

Proof

Step	Hyp	Ref	Expression
1		parcoval.m	|- M = ( f e. K , g e. K |-> ( f i^i g ) )
2		parcoval.c	|- .x. = ( p e. ( B X. B ) , z e. B |-> M )
3		parcoval.s	|- M e. _V
4		parcoval.u	|- ( ph -> U e. B )
5		parcoval.v	|- ( ph -> V e. B )
6		parcoval.w	|- ( ph -> W e. B )
7		parcoval.f	|- ( ph -> F e. K )
8		parcoval.g	|- ( ph -> G e. K )
9	2	a1i	|- ( ph -> .x. = ( p e. ( B X. B ) , z e. B |-> M ) )
10		eqidd	|- ( ( ph /\ ( p = <. U , V >. /\ z = W ) ) -> M = M )
11	4 5	opelxpd	|- ( ph -> <. U , V >. e. ( B X. B ) )
12	3	a1i	|- ( ph -> M e. _V )
13	9 10 11 6 12	ovmpod	|- ( ph -> ( <. U , V >. .x. W ) = M )
14	13	oveqd	|- ( ph -> ( G ( <. U , V >. .x. W ) F ) = ( G M F ) )
15	1	a1i	|- ( ph -> M = ( f e. K , g e. K |-> ( f i^i g ) ) )
16		simprl	|- ( ( ph /\ ( f = G /\ g = F ) ) -> f = G )
17		simprr	|- ( ( ph /\ ( f = G /\ g = F ) ) -> g = F )
18	16 17	ineq12d	|- ( ( ph /\ ( f = G /\ g = F ) ) -> ( f i^i g ) = ( G i^i F ) )
19		inex1g	|- ( G e. K -> ( G i^i F ) e. _V )
20	8 19	syl	|- ( ph -> ( G i^i F ) e. _V )
21	15 18 8 7 20	ovmpod	|- ( ph -> ( G M F ) = ( G i^i F ) )
22	14 21	eqtrd	|- ( ph -> ( G ( <. U , V >. .x. W ) F ) = ( G i^i F ) )