Theorem coss2b

Description: Postcomposition with an injective class (see cocnv1ssid ) preserves and reflects the subclass relation up to corestriction to its domain. This is a generalization of the fact that injections are left-cancellable. Compare with coss1b . There is no special syntax for corestriction as explained in the comment of df-res . (Contributed by BJ, 24-Oct-2026) TODO: prove cocanss1 from it.

	Ref	Expression
Hypothesis	coss2b.1	$$⊢\phi \to F^{-1}\circ F\subseteq \mathrm{I}$$
Assertion	coss2b	$$⊢\phi \to \left(F\circ H\subseteq F\circ K\leftrightarrow H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		coss2b.1	$$⊢\phi \to F^{-1}\circ F\subseteq \mathrm{I}$$
2		coss2	$$⊢F\circ H\subseteq F\circ K\to F^{-1}\circ \left(F\circ H\right)\subseteq F^{-1}\circ \left(F\circ K\right)$$
3		coass	$$⊢\left(F^{-1}\circ F\right)\circ H=F^{-1}\circ \left(F\circ H\right)$$
4		iss	$$⊢F^{-1}\circ F\subseteq \mathrm{I}\leftrightarrow F^{-1}\circ F={\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F^{-1}\circ F\right)}$$
5	1 4	sylib	$$⊢\phi \to F^{-1}\circ F={\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F^{-1}\circ F\right)}$$
6		dmcocnv1	$$⊢\mathrm{dom}\left(F^{-1}\circ F\right)=\mathrm{dom}F$$
7	6	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}\left(F^{-1}\circ F\right)}={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
8	5 7	eqtrdi	$$⊢\phi \to F^{-1}\circ F={\mathrm{I}\upharpoonright }_{\mathrm{dom}F}$$
9	8	coeq1d	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ H=\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\circ H$$
10		coires2	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\circ H=H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
11	9 10	eqtrdi	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ H=H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
12	3 11	eqtr3id	$$⊢\phi \to F^{-1}\circ \left(F\circ H\right)=H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
13		coass	$$⊢\left(F^{-1}\circ F\right)\circ K=F^{-1}\circ \left(F\circ K\right)$$
14	8	coeq1d	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ K=\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\circ K$$
15		coires2	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}F}\right)\circ K=K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
16	14 15	eqtrdi	$$⊢\phi \to \left(F^{-1}\circ F\right)\circ K=K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
17	13 16	eqtr3id	$$⊢\phi \to F^{-1}\circ \left(F\circ K\right)=K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
18	12 17	sseq12d	$$⊢\phi \to \left(F^{-1}\circ \left(F\circ H\right)\subseteq F^{-1}\circ \left(F\circ K\right)\leftrightarrow H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$
19	2 18	imbitrid	$$⊢\phi \to \left(F\circ H\subseteq F\circ K\to H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$
20		coss2	$$⊢H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\to F\circ \left(H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)\subseteq F\circ \left(K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$
21		cnvrescnv	$$⊢{\left({H^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
22	21	coeq2i	$$⊢F\circ {\left({H^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ \left(H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$
23		ssid	$$⊢\mathrm{dom}F\subseteq \mathrm{dom}F$$
24		cores2	$$⊢\mathrm{dom}F\subseteq \mathrm{dom}F\to F\circ {\left({H^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ H$$
25	23 24	ax-mp	$$⊢F\circ {\left({H^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ H$$
26	22 25	eqtr3i	$$⊢F\circ \left(H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)=F\circ H$$
27		cnvrescnv	$$⊢{\left({K^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)$$
28	27	coeq2i	$$⊢F\circ {\left({K^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ \left(K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$
29		cores2	$$⊢\mathrm{dom}F\subseteq \mathrm{dom}F\to F\circ {\left({K^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ K$$
30	23 29	ax-mp	$$⊢F\circ {\left({K^{-1}\upharpoonright }_{\mathrm{dom}F}\right)}^{-1}=F\circ K$$
31	28 30	eqtr3i	$$⊢F\circ \left(K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)=F\circ K$$
32	20 26 31	3sstr3g	$$⊢H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\to F\circ H\subseteq F\circ K$$
33	19 32	impbid1	$$⊢\phi \to \left(F\circ H\subseteq F\circ K\leftrightarrow H\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\subseteq K\cap \left(\mathrm{V}\times \mathrm{dom}F\right)\right)$$