Theorem cocan2g

Description: Cancellation law for composition. A version of cocan2 with weaker hypotheses. (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Hypotheses	cocan2g.1	$$⊢\phi \to \mathrm{Fun}F$$
	cocan2g.2	$$⊢\phi \to \mathrm{Rel}H$$
	cocan2g.3	$$⊢\phi \to \mathrm{dom}H\subseteq \mathrm{ran}F$$
	cocan2g.4	$$⊢\phi \to \mathrm{Rel}K$$
	cocan2g.5	$$⊢\phi \to \mathrm{dom}K\subseteq \mathrm{ran}F$$
Assertion	cocan2g	$$⊢\phi \to \left(H\circ F=K\circ F\leftrightarrow H=K\right)$$

Proof

Step	Hyp	Ref	Expression
1		cocan2g.1	$$⊢\phi \to \mathrm{Fun}F$$
2		cocan2g.2	$$⊢\phi \to \mathrm{Rel}H$$
3		cocan2g.3	$$⊢\phi \to \mathrm{dom}H\subseteq \mathrm{ran}F$$
4		cocan2g.4	$$⊢\phi \to \mathrm{Rel}K$$
5		cocan2g.5	$$⊢\phi \to \mathrm{dom}K\subseteq \mathrm{ran}F$$
6	1 2 3	cocanss2	$$⊢\phi \to \left(H\circ F\subseteq K\circ F\leftrightarrow H\subseteq K\right)$$
7	1 4 5	cocanss2	$$⊢\phi \to \left(K\circ F\subseteq H\circ F\leftrightarrow K\subseteq H\right)$$
8	6 7	anbi12d	$$⊢\phi \to \left(\left(H\circ F\subseteq K\circ F\wedge K\circ F\subseteq H\circ F\right)\leftrightarrow \left(H\subseteq K\wedge K\subseteq H\right)\right)$$
9		eqss	$$⊢H\circ F=K\circ F\leftrightarrow \left(H\circ F\subseteq K\circ F\wedge K\circ F\subseteq H\circ F\right)$$
10		eqss	$$⊢H=K\leftrightarrow \left(H\subseteq K\wedge K\subseteq H\right)$$
11	8 9 10	3bitr4g	$$⊢\phi \to \left(H\circ F=K\circ F\leftrightarrow H=K\right)$$