parmapco2

Description: Variant of parmapco . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026) (New usage is discouraged.) (Proof modification is discouraged.)

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

Metamath Proof Explorer

Theorem parmapco2

Proof