parhomco2

Description: Variant of parhomco . (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	parhomval.h	$⊢ H = (x \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
	parhomeqor.f	$⊢ φ \to F \in (U H V)$
	parhomeqor.g	$⊢ φ \to G \in (V H W)$
	parhomco.p	$⊢ S \subseteq 𝒫 J$
	parhomco2.s	$⊢ S \in V$
	parhomco2.j	$⊢ J \in V$
	parhomco2.n	$⊢ X \neq Y$
	parhomco2.u	$⊢ φ \to U \in B$
	parhomco2.v	$⊢ φ \to V \in B$
	parhomco2.w	$⊢ φ \to W \in B$
Assertion	parhomco2	$⊢ φ \to G \cap F \in (U H W)$

Proof

Step	Hyp	Ref	Expression
1		parhomval.h	$⊢ H = (x \in B, y \in B ⟼ if (x = y, \{J\}, if ((x = X \land y = Y), S, \emptyset)))$
2		parhomeqor.f	$⊢ φ \to F \in (U H V)$
3		parhomeqor.g	$⊢ φ \to G \in (V H W)$
4		parhomco.p	$⊢ S \subseteq 𝒫 J$
5		parhomco2.s	$⊢ S \in V$
6		parhomco2.j	$⊢ J \in V$
7		parhomco2.n	$⊢ X \neq Y$
8		parhomco2.u	$⊢ φ \to U \in B$
9		parhomco2.v	$⊢ φ \to V \in B$
10		parhomco2.w	$⊢ φ \to W \in B$
11	3	adantr	$⊢ (φ \land U = V) \to G \in (V H W)$
12	2	adantr	$⊢ (φ \land U = V) \to F \in (U H V)$
13		simpr	$⊢ (φ \land U = V) \to U = V$
14	1 12 13	parhomideq	$⊢ (φ \land U = V) \to F = J$
15	14	ineq2d	$⊢ (φ \land U = V) \to G \cap F = G \cap J$
16	1 4 3	parhomss	$⊢ φ \to G \subseteq J$
17	16	adantr	$⊢ (φ \land U = V) \to G \subseteq J$
18		dfss2	$⊢ G \subseteq J \leftrightarrow G \cap J = G$
19	17 18	sylib	$⊢ (φ \land U = V) \to G \cap J = G$
20	15 19	eqtrd	$⊢ (φ \land U = V) \to G \cap F = G$
21	13	oveq1d	$⊢ (φ \land U = V) \to U H W = V H W$
22	11 20 21	3eltr4d	$⊢ (φ \land U = V) \to G \cap F \in (U H W)$
23	3	adantr	$⊢ (φ \land V = W) \to G \in (V H W)$
24		simpr	$⊢ (φ \land V = W) \to V = W$
25	1 23 24	parhomideq	$⊢ (φ \land V = W) \to G = J$
26	25	ineq1d	$⊢ (φ \land V = W) \to G \cap F = J \cap F$
27	1 4 2	parhomss	$⊢ φ \to F \subseteq J$
28	27	adantr	$⊢ (φ \land V = W) \to F \subseteq J$
29		sseqin2	$⊢ F \subseteq J \leftrightarrow J \cap F = F$
30	28 29	sylib	$⊢ (φ \land V = W) \to J \cap F = F$
31	26 30	eqtrd	$⊢ (φ \land V = W) \to G \cap F = F$
32	2	adantr	$⊢ (φ \land V = W) \to F \in (U H V)$
33	24	oveq2d	$⊢ (φ \land V = W) \to U H V = U H W$
34	32 33	eleqtrd	$⊢ (φ \land V = W) \to F \in (U H W)$
35	31 34	eqeltrd	$⊢ (φ \land V = W) \to G \cap F \in (U H W)$
36	1 2 3	parhomeqor	$⊢ φ \to (U = V \lor V = W)$
37	22 35 36	mpjaodan	$⊢ φ \to G \cap F \in (U H W)$

Metamath Proof Explorer

Theorem parhomco2

Proof