Theorem cocan1g

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

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

Proof

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