Theorem coss1b

Description: Precomposition with a single-valued class (see cocnv2ssid ) preserves and reflects the subclass relation on its range. This is a generalization of the fact that surjections are right-cancellable. (Contributed by BJ, 24-Oct-2026) TODO: prove cocanss2 from it.

	Ref	Expression
Hypothesis	coss1b.1	$$⊢\phi \to F\circ F^{-1}\subseteq \mathrm{I}$$
Assertion	coss1b	$$⊢\phi \to \left(H\circ F\subseteq K\circ F\leftrightarrow {H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\right)$$

Proof

Step	Hyp	Ref	Expression
1		coss1b.1	$$⊢\phi \to F\circ F^{-1}\subseteq \mathrm{I}$$
2		coss1	$$⊢H\circ F\subseteq K\circ F\to \left(H\circ F\right)\circ F^{-1}\subseteq \left(K\circ F\right)\circ F^{-1}$$
3		coass	$$⊢\left(H\circ F\right)\circ F^{-1}=H\circ \left(F\circ F^{-1}\right)$$
4		iss	$$⊢F\circ F^{-1}\subseteq \mathrm{I}\leftrightarrow F\circ F^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F\circ F^{-1}\right)}$$
5	1 4	sylib	$$⊢\phi \to F\circ F^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F\circ F^{-1}\right)}$$
6		dmcocnv2	$$⊢\mathrm{dom}\left(F\circ F^{-1}\right)=\mathrm{ran}F$$
7	6	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F\circ F^{-1}\right)}={\mathrm{I}\upharpoonright }_{\mathrm{ran}F}$$
8	5 7	eqtrdi	$$⊢\phi \to F\circ F^{-1}={\mathrm{I}\upharpoonright }_{\mathrm{ran}F}$$
9	8	coeq2d	$$⊢\phi \to H\circ \left(F\circ F^{-1}\right)=H\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)$$
10		coires1	$$⊢H\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)={H\upharpoonright }_{\mathrm{ran}F}$$
11	9 10	eqtrdi	$$⊢\phi \to H\circ \left(F\circ F^{-1}\right)={H\upharpoonright }_{\mathrm{ran}F}$$
12	3 11	eqtrid	$$⊢\phi \to \left(H\circ F\right)\circ F^{-1}={H\upharpoonright }_{\mathrm{ran}F}$$
13		coass	$$⊢\left(K\circ F\right)\circ F^{-1}=K\circ \left(F\circ F^{-1}\right)$$
14	8	coeq2d	$$⊢\phi \to K\circ \left(F\circ F^{-1}\right)=K\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)$$
15		coires1	$$⊢K\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{ran}F}\right)={K\upharpoonright }_{\mathrm{ran}F}$$
16	14 15	eqtrdi	$$⊢\phi \to K\circ \left(F\circ F^{-1}\right)={K\upharpoonright }_{\mathrm{ran}F}$$
17	13 16	eqtrid	$$⊢\phi \to \left(K\circ F\right)\circ F^{-1}={K\upharpoonright }_{\mathrm{ran}F}$$
18	12 17	sseq12d	$$⊢\phi \to \left(\left(H\circ F\right)\circ F^{-1}\subseteq \left(K\circ F\right)\circ F^{-1}\leftrightarrow {H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\right)$$
19	2 18	imbitrid	$$⊢\phi \to \left(H\circ F\subseteq K\circ F\to {H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\right)$$
20		coss1	$$⊢{H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\to \left({H\upharpoonright }_{\mathrm{ran}F}\right)\circ F\subseteq \left({K\upharpoonright }_{\mathrm{ran}F}\right)\circ F$$
21		coresrn	$$⊢\left({H\upharpoonright }_{\mathrm{ran}F}\right)\circ F=H\circ F$$
22		coresrn	$$⊢\left({K\upharpoonright }_{\mathrm{ran}F}\right)\circ F=K\circ F$$
23	20 21 22	3sstr3g	$$⊢{H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\to H\circ F\subseteq K\circ F$$
24	19 23	impbid1	$$⊢\phi \to \left(H\circ F\subseteq K\circ F\leftrightarrow {H\upharpoonright }_{\mathrm{ran}F}\subseteq {K\upharpoonright }_{\mathrm{ran}F}\right)$$