Theorem cocanss1

Description: Cancellation law for composition. Suggested by BJ. (Contributed by Eric Schmidt, 30-Sep-2026)

	Ref	Expression
Hypotheses	cocan1g.1	|- ( ph -> Fun `' F )
	cocan1g.2	|- ( ph -> Rel H )
	cocan1g.3	|- ( ph -> ran H C_ dom F )
Assertion	cocanss1	|- ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> H C_ K ) )

Proof

Step	Hyp	Ref	Expression
1		cocan1g.1	|- ( ph -> Fun `' F )
2		cocan1g.2	|- ( ph -> Rel H )
3		cocan1g.3	|- ( ph -> ran H C_ dom F )
4		relcnv	|- Rel `' H
5	4	a1i	|- ( ph -> Rel `' H )
6		df-rn	|- ran H = dom `' H
7		dfdm4	|- dom F = ran `' F
8	3 6 7	3sstr3g	|- ( ph -> dom `' H C_ ran `' F )
9	1 5 8	cocanss2	|- ( ph -> ( ( `' H o. `' F ) C_ ( `' K o. `' F ) <-> `' H C_ `' K ) )
10		relco	|- Rel ( F o. H )
11		cnvssb	|- ( Rel ( F o. H ) -> ( ( F o. H ) C_ ( F o. K ) <-> `' ( F o. H ) C_ `' ( F o. K ) ) )
12	10 11	ax-mp	|- ( ( F o. H ) C_ ( F o. K ) <-> `' ( F o. H ) C_ `' ( F o. K ) )
13		cnvco	|- `' ( F o. H ) = ( `' H o. `' F )
14		cnvco	|- `' ( F o. K ) = ( `' K o. `' F )
15	13 14	sseq12i	|- ( `' ( F o. H ) C_ `' ( F o. K ) <-> ( `' H o. `' F ) C_ ( `' K o. `' F ) )
16	12 15	bitri	|- ( ( F o. H ) C_ ( F o. K ) <-> ( `' H o. `' F ) C_ ( `' K o. `' F ) )
17	16	a1i	|- ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> ( `' H o. `' F ) C_ ( `' K o. `' F ) ) )
18		cnvssb	|- ( Rel H -> ( H C_ K <-> `' H C_ `' K ) )
19	2 18	syl	|- ( ph -> ( H C_ K <-> `' H C_ `' K ) )
20	9 17 19	3bitr4d	|- ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> H C_ K ) )