Theorem cocan2g

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

	Ref	Expression
Hypotheses	cocan2g.1	|- ( ph -> Fun F )
	cocan2g.2	|- ( ph -> Rel H )
	cocan2g.3	|- ( ph -> dom H C_ ran F )
	cocan2g.4	|- ( ph -> Rel K )
	cocan2g.5	|- ( ph -> dom K C_ ran F )
Assertion	cocan2g	|- ( ph -> ( ( H o. F ) = ( K o. F ) <-> H = K ) )

Proof

Step	Hyp	Ref	Expression
1		cocan2g.1	|- ( ph -> Fun F )
2		cocan2g.2	|- ( ph -> Rel H )
3		cocan2g.3	|- ( ph -> dom H C_ ran F )
4		cocan2g.4	|- ( ph -> Rel K )
5		cocan2g.5	|- ( ph -> dom K C_ ran F )
6	1 2 3	cocanss2	|- ( ph -> ( ( H o. F ) C_ ( K o. F ) <-> H C_ K ) )
7	1 4 5	cocanss2	|- ( ph -> ( ( K o. F ) C_ ( H o. F ) <-> K C_ H ) )
8	6 7	anbi12d	|- ( ph -> ( ( ( H o. F ) C_ ( K o. F ) /\ ( K o. F ) C_ ( H o. F ) ) <-> ( H C_ K /\ K C_ H ) ) )
9		eqss	|- ( ( H o. F ) = ( K o. F ) <-> ( ( H o. F ) C_ ( K o. F ) /\ ( K o. F ) C_ ( H o. F ) ) )
10		eqss	|- ( H = K <-> ( H C_ K /\ K C_ H ) )
11	8 9 10	3bitr4g	|- ( ph -> ( ( H o. F ) = ( K o. F ) <-> H = K ) )