parmapco

Description: An identity-fixing map preserving parallel arrows preserves every typed composition. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	parmapcl.h	$⊢ H = (x \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
	parmapco.p	$⊢ S \subseteq 𝒫 J$
	parmapco.f	$⊢ φ \to F \in (U H V)$
	parmapco.g	$⊢ φ \to G \in (V H W)$
	parmapco.i	$⊢ φ \to A (J) = J$
	parmapco.a	$⊢ (φ \land F \in S) \to A (F) \in S$
	parmapco.b	$⊢ (φ \land G \in S) \to A (G) \in S$
Assertion	parmapco	$⊢ φ \to A (G \cap F) = A (G) \cap A (F)$

Proof

Step	Hyp	Ref	Expression
1		parmapcl.h	$⊢ H = (x \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
2		parmapco.p	$⊢ S \subseteq 𝒫 J$
3		parmapco.f	$⊢ φ \to F \in (U H V)$
4		parmapco.g	$⊢ φ \to G \in (V H W)$
5		parmapco.i	$⊢ φ \to A (J) = J$
6		parmapco.a	$⊢ (φ \land F \in S) \to A (F) \in S$
7		parmapco.b	$⊢ (φ \land G \in S) \to A (G) \in S$
8	1 4 5 7	parmapcl	$⊢ φ \to A (G) \in (V H W)$
9	1 2 8	parhomss	$⊢ φ \to A (G) \subseteq J$
10	9	adantr	$⊢ (φ \land U = V) \to A (G) \subseteq J$
11		dfss2	$⊢ A (G) \subseteq J \leftrightarrow A (G) \cap J = A (G)$
12	10 11	sylib	$⊢ (φ \land U = V) \to A (G) \cap J = A (G)$
13	3	adantr	$⊢ (φ \land U = V) \to F \in (U H V)$
14		simpr	$⊢ (φ \land U = V) \to U = V$
15	1 13 14	parhomideq	$⊢ (φ \land U = V) \to F = J$
16	15	fveq2d	$⊢ (φ \land U = V) \to A (F) = A (J)$
17	5	adantr	$⊢ (φ \land U = V) \to A (J) = J$
18	16 17	eqtrd	$⊢ (φ \land U = V) \to A (F) = J$
19	18	ineq2d	$⊢ (φ \land U = V) \to A (G) \cap A (F) = A (G) \cap J$
20	15	ineq2d	$⊢ (φ \land U = V) \to G \cap F = G \cap J$
21	1 2 4	parhomss	$⊢ φ \to G \subseteq J$
22	21	adantr	$⊢ (φ \land U = V) \to G \subseteq J$
23		dfss2	$⊢ G \subseteq J \leftrightarrow G \cap J = G$
24	22 23	sylib	$⊢ (φ \land U = V) \to G \cap J = G$
25	20 24	eqtrd	$⊢ (φ \land U = V) \to G \cap F = G$
26	25	fveq2d	$⊢ (φ \land U = V) \to A (G \cap F) = A (G)$
27	12 19 26	3eqtr4rd	$⊢ (φ \land U = V) \to A (G \cap F) = A (G) \cap A (F)$
28	1 3 5 6	parmapcl	$⊢ φ \to A (F) \in (U H V)$
29	1 2 28	parhomss	$⊢ φ \to A (F) \subseteq J$
30	29	adantr	$⊢ (φ \land V = W) \to A (F) \subseteq J$
31		sseqin2	$⊢ A (F) \subseteq J \leftrightarrow J \cap A (F) = A (F)$
32	30 31	sylib	$⊢ (φ \land V = W) \to J \cap A (F) = A (F)$
33	4	adantr	$⊢ (φ \land V = W) \to G \in (V H W)$
34		simpr	$⊢ (φ \land V = W) \to V = W$
35	1 33 34	parhomideq	$⊢ (φ \land V = W) \to G = J$
36	35	fveq2d	$⊢ (φ \land V = W) \to A (G) = A (J)$
37	5	adantr	$⊢ (φ \land V = W) \to A (J) = J$
38	36 37	eqtrd	$⊢ (φ \land V = W) \to A (G) = J$
39	38	ineq1d	$⊢ (φ \land V = W) \to A (G) \cap A (F) = J \cap A (F)$
40	35	ineq1d	$⊢ (φ \land V = W) \to G \cap F = J \cap F$
41	1 2 3	parhomss	$⊢ φ \to F \subseteq J$
42	41	adantr	$⊢ (φ \land V = W) \to F \subseteq J$
43		sseqin2	$⊢ F \subseteq J \leftrightarrow J \cap F = F$
44	42 43	sylib	$⊢ (φ \land V = W) \to J \cap F = F$
45	40 44	eqtrd	$⊢ (φ \land V = W) \to G \cap F = F$
46	45	fveq2d	$⊢ (φ \land V = W) \to A (G \cap F) = A (F)$
47	32 39 46	3eqtr4rd	$⊢ (φ \land V = W) \to A (G \cap F) = A (G) \cap A (F)$
48	1 3 4	parhomeqor	$⊢ φ \to (U = V \lor V = W)$
49	27 47 48	mpjaodan	$⊢ φ \to A (G \cap F) = A (G) \cap A (F)$

Metamath Proof Explorer

Theorem parmapco

Proof