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	|- ( ph -> ( F o. `' F ) C_ _I )
Assertion	coss1b	|- ( ph -> ( ( H o. F ) C_ ( K o. F ) <-> ( H |` ran F ) C_ ( K |` ran F ) ) )

Proof

Step	Hyp	Ref	Expression
1		coss1b.1	|- ( ph -> ( F o. `' F ) C_ _I )
2		coss1	|- ( ( H o. F ) C_ ( K o. F ) -> ( ( H o. F ) o. `' F ) C_ ( ( K o. F ) o. `' F ) )
3		coass	|- ( ( H o. F ) o. `' F ) = ( H o. ( F o. `' F ) )
4		iss	|- ( ( F o. `' F ) C_ _I <-> ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) )
5	1 4	sylib	|- ( ph -> ( F o. `' F ) = ( _I |` dom ( F o. `' F ) ) )
6		dmcocnv2	|- dom ( F o. `' F ) = ran F
7	6	reseq2i	|- ( _I |` dom ( F o. `' F ) ) = ( _I |` ran F )
8	5 7	eqtrdi	|- ( ph -> ( F o. `' F ) = ( _I |` ran F ) )
9	8	coeq2d	|- ( ph -> ( H o. ( F o. `' F ) ) = ( H o. ( _I |` ran F ) ) )
10		coires1	|- ( H o. ( _I |` ran F ) ) = ( H |` ran F )
11	9 10	eqtrdi	|- ( ph -> ( H o. ( F o. `' F ) ) = ( H |` ran F ) )
12	3 11	eqtrid	|- ( ph -> ( ( H o. F ) o. `' F ) = ( H |` ran F ) )
13		coass	|- ( ( K o. F ) o. `' F ) = ( K o. ( F o. `' F ) )
14	8	coeq2d	|- ( ph -> ( K o. ( F o. `' F ) ) = ( K o. ( _I |` ran F ) ) )
15		coires1	|- ( K o. ( _I |` ran F ) ) = ( K |` ran F )
16	14 15	eqtrdi	|- ( ph -> ( K o. ( F o. `' F ) ) = ( K |` ran F ) )
17	13 16	eqtrid	|- ( ph -> ( ( K o. F ) o. `' F ) = ( K |` ran F ) )
18	12 17	sseq12d	|- ( ph -> ( ( ( H o. F ) o. `' F ) C_ ( ( K o. F ) o. `' F ) <-> ( H |` ran F ) C_ ( K |` ran F ) ) )
19	2 18	imbitrid	|- ( ph -> ( ( H o. F ) C_ ( K o. F ) -> ( H |` ran F ) C_ ( K |` ran F ) ) )
20		coss1	|- ( ( H |` ran F ) C_ ( K |` ran F ) -> ( ( H |` ran F ) o. F ) C_ ( ( K |` ran F ) o. F ) )
21		coresrn	|- ( ( H |` ran F ) o. F ) = ( H o. F )
22		coresrn	|- ( ( K |` ran F ) o. F ) = ( K o. F )
23	20 21 22	3sstr3g	|- ( ( H |` ran F ) C_ ( K |` ran F ) -> ( H o. F ) C_ ( K o. F ) )
24	19 23	impbid1	|- ( ph -> ( ( H o. F ) C_ ( K o. F ) <-> ( H |` ran F ) C_ ( K |` ran F ) ) )