cocanss1

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

	Ref	Expression
Hypotheses	cocan1g.1	$⊢ φ \to Fun F^{-1}$
	cocan1g.2	$⊢ φ \to Rel H$
	cocan1g.3	$⊢ φ \to ran H \subseteq dom F$
Assertion	cocanss1	$⊢ φ \to (F \circ H \subseteq F \circ K \leftrightarrow H \subseteq K)$

Step	Hyp	Ref	Expression
1		cocan1g.1	$⊢ φ \to Fun F^{-1}$
2		cocan1g.2	$⊢ φ \to Rel H$
3		cocan1g.3	$⊢ φ \to ran H \subseteq dom F$
4		relcnv	$⊢ Rel H^{-1}$
5	4	a1i	$⊢ φ \to Rel H^{-1}$
6		df-rn	$⊢ ran H = dom H^{-1}$
7		dfdm4	$⊢ dom F = ran F^{-1}$
8	3 6 7	3sstr3g	$⊢ φ \to dom H^{-1} \subseteq ran F^{-1}$
9	1 5 8	cocanss2	$⊢ φ \to (H^{-1} \circ F^{-1} \subseteq K^{-1} \circ F^{-1} \leftrightarrow H^{-1} \subseteq K^{-1})$
10		relco	$⊢ Rel (F \circ H)$
11		cnvssb	$⊢ Rel (F \circ H) \to (F \circ H \subseteq F \circ K \leftrightarrow {(F \circ H)}^{-1} \subseteq {(F \circ K)}^{-1})$
12	10 11	ax-mp	$⊢ F \circ H \subseteq F \circ K \leftrightarrow {(F \circ H)}^{-1} \subseteq {(F \circ K)}^{-1}$
13		cnvco	$⊢ {(F \circ H)}^{-1} = H^{-1} \circ F^{-1}$
14		cnvco	$⊢ {(F \circ K)}^{-1} = K^{-1} \circ F^{-1}$
15	13 14	sseq12i	$⊢ {(F \circ H)}^{-1} \subseteq {(F \circ K)}^{-1} \leftrightarrow H^{-1} \circ F^{-1} \subseteq K^{-1} \circ F^{-1}$
16	12 15	bitri	$⊢ F \circ H \subseteq F \circ K \leftrightarrow H^{-1} \circ F^{-1} \subseteq K^{-1} \circ F^{-1}$
17	16	a1i	$⊢ φ \to (F \circ H \subseteq F \circ K \leftrightarrow H^{-1} \circ F^{-1} \subseteq K^{-1} \circ F^{-1})$
18		cnvssb	$⊢ Rel H \to (H \subseteq K \leftrightarrow H^{-1} \subseteq K^{-1})$
19	2 18	syl	$⊢ φ \to (H \subseteq K \leftrightarrow H^{-1} \subseteq K^{-1})$
20	9 17 19	3bitr4d	$⊢ φ \to (F \circ H \subseteq F \circ K \leftrightarrow H \subseteq K)$

Metamath Proof Explorer