parhomco

Description: When every member of the parallel-arrow class S is a subset of J , intersection of composable arrows belongs to the hom-set from the first object to the last. The subset hypothesis supplies the required intersection identity laws; it does not follow from the hom construction alone. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	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$
Assertion	parhomco	$⊢ φ \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	3	adantr	$⊢ (φ \land U = V) \to G \in (V H W)$
6	2	adantr	$⊢ (φ \land U = V) \to F \in (U H V)$
7		simpr	$⊢ (φ \land U = V) \to U = V$
8	1 6 7	parhomideq	$⊢ (φ \land U = V) \to F = J$
9	8	ineq2d	$⊢ (φ \land U = V) \to G \cap F = G \cap J$
10	1 4 3	parhomss	$⊢ φ \to G \subseteq J$
11	10	adantr	$⊢ (φ \land U = V) \to G \subseteq J$
12		dfss2	$⊢ G \subseteq J \leftrightarrow G \cap J = G$
13	11 12	sylib	$⊢ (φ \land U = V) \to G \cap J = G$
14	9 13	eqtrd	$⊢ (φ \land U = V) \to G \cap F = G$
15	7	oveq1d	$⊢ (φ \land U = V) \to U H W = V H W$
16	5 14 15	3eltr4d	$⊢ (φ \land U = V) \to G \cap F \in (U H W)$
17	3	adantr	$⊢ (φ \land V = W) \to G \in (V H W)$
18		simpr	$⊢ (φ \land V = W) \to V = W$
19	1 17 18	parhomideq	$⊢ (φ \land V = W) \to G = J$
20	19	ineq1d	$⊢ (φ \land V = W) \to G \cap F = J \cap F$
21	1 4 2	parhomss	$⊢ φ \to F \subseteq J$
22	21	adantr	$⊢ (φ \land V = W) \to F \subseteq J$
23		sseqin2	$⊢ F \subseteq J \leftrightarrow J \cap F = F$
24	22 23	sylib	$⊢ (φ \land V = W) \to J \cap F = F$
25	20 24	eqtrd	$⊢ (φ \land V = W) \to G \cap F = F$
26	2	adantr	$⊢ (φ \land V = W) \to F \in (U H V)$
27	18	oveq2d	$⊢ (φ \land V = W) \to U H V = U H W$
28	26 27	eleqtrd	$⊢ (φ \land V = W) \to F \in (U H W)$
29	25 28	eqeltrd	$⊢ (φ \land V = W) \to G \cap F \in (U H W)$
30	1 2 3	parhomeqor	$⊢ φ \to (U = V \lor V = W)$
31	16 29 30	mpjaodan	$⊢ φ \to G \cap F \in (U H W)$

Metamath Proof Explorer

Theorem parhomco

Proof