cocanss2

Description: Cancellation law for composition. Suggested by BJ. (Contributed by Eric Schmidt, 30-Sep-2026)

	Ref	Expression
Hypotheses	cocan2g.1	$⊢ φ \to Fun F$
	cocan2g.2	$⊢ φ \to Rel H$
	cocan2g.3	$⊢ φ \to dom H \subseteq ran F$
Assertion	cocanss2	$⊢ φ \to (H \circ F \subseteq K \circ F \leftrightarrow H \subseteq K)$

Proof

Step	Hyp	Ref	Expression
1		cocan2g.1	$⊢ φ \to Fun F$
2		cocan2g.2	$⊢ φ \to Rel H$
3		cocan2g.3	$⊢ φ \to dom H \subseteq ran F$
4	2	adantr	$⊢ (φ \land H \circ F \subseteq K \circ F) \to Rel H$
5		vex	$⊢ y \in V$
6		vex	$⊢ z \in V$
7	5 6	breldm	$⊢ y H z \to y \in dom H$
8	3	sseld	$⊢ φ \to (y \in dom H \to y \in ran F)$
9	7 8	syl5	$⊢ φ \to (y H z \to y \in ran F)$
10	5	elrn	$⊢ y \in ran F \leftrightarrow \exists x x F y$
11	9 10	imbitrdi	$⊢ φ \to (y H z \to \exists x x F y)$
12	11	adantr	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (y H z \to \exists x x F y)$
13		19.8a	$⊢ (x F y \land y H z) \to \exists y (x F y \land y H z)$
14		vex	$⊢ x \in V$
15	14 6	brco	$⊢ x (H \circ F) z \leftrightarrow \exists y (x F y \land y H z)$
16	13 15	sylibr	$⊢ (x F y \land y H z) \to x (H \circ F) z$
17		ssbr	$⊢ H \circ F \subseteq K \circ F \to (x (H \circ F) z \to x (K \circ F) z)$
18	16 17	syl5	$⊢ H \circ F \subseteq K \circ F \to ((x F y \land y H z) \to x (K \circ F) z)$
19	14 6	brco	$⊢ x (K \circ F) z \leftrightarrow \exists w (x F w \land w K z)$
20	18 19	imbitrdi	$⊢ H \circ F \subseteq K \circ F \to ((x F y \land y H z) \to \exists w (x F w \land w K z))$
21	20	adantl	$⊢ (φ \land H \circ F \subseteq K \circ F) \to ((x F y \land y H z) \to \exists w (x F w \land w K z))$
22		vex	$⊢ w \in V$
23	14 5 22	fununiq	$⊢ Fun F \to ((x F y \land x F w) \to y = w)$
24	23	imp	$⊢ (Fun F \land (x F y \land x F w)) \to y = w$
25	24	breq1d	$⊢ (Fun F \land (x F y \land x F w)) \to (y K z \leftrightarrow w K z)$
26	25	biimprd	$⊢ (Fun F \land (x F y \land x F w)) \to (w K z \to y K z)$
27	26	expr	$⊢ (Fun F \land x F y) \to (x F w \to (w K z \to y K z))$
28	27	impd	$⊢ (Fun F \land x F y) \to ((x F w \land w K z) \to y K z)$
29	28	exlimdv	$⊢ (Fun F \land x F y) \to (\exists w (x F w \land w K z) \to y K z)$
30	1 29	sylan	$⊢ (φ \land x F y) \to (\exists w (x F w \land w K z) \to y K z)$
31	30	ex	$⊢ φ \to (x F y \to (\exists w (x F w \land w K z) \to y K z))$
32	31	adantr	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (x F y \to (\exists w (x F w \land w K z) \to y K z))$
33	32	adantrd	$⊢ (φ \land H \circ F \subseteq K \circ F) \to ((x F y \land y H z) \to (\exists w (x F w \land w K z) \to y K z))$
34	21 33	mpdd	$⊢ (φ \land H \circ F \subseteq K \circ F) \to ((x F y \land y H z) \to y K z)$
35	34	expd	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (x F y \to (y H z \to y K z))$
36	35	exlimdv	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (\exists x x F y \to (y H z \to y K z))$
37	36	com23	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (y H z \to (\exists x x F y \to y K z))$
38	12 37	mpdd	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (y H z \to y K z)$
39		df-br	$⊢ y H z \leftrightarrow ⟨y, z⟩ \in H$
40		df-br	$⊢ y K z \leftrightarrow ⟨y, z⟩ \in K$
41	38 39 40	3imtr3g	$⊢ (φ \land H \circ F \subseteq K \circ F) \to (⟨y, z⟩ \in H \to ⟨y, z⟩ \in K)$
42	4 41	relssdv	$⊢ (φ \land H \circ F \subseteq K \circ F) \to H \subseteq K$
43	42	ex	$⊢ φ \to (H \circ F \subseteq K \circ F \to H \subseteq K)$
44		coss1	$⊢ H \subseteq K \to H \circ F \subseteq K \circ F$
45	43 44	impbid1	$⊢ φ \to (H \circ F \subseteq K \circ F \leftrightarrow H \subseteq K)$

Metamath Proof Explorer

Theorem cocanss2

Proof