Theorem cocan1g

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

	Ref	Expression
Hypotheses	cocan1g.1	|- ( ph -> Fun `' F )
	cocan1g.2	|- ( ph -> Rel H )
	cocan1g.3	|- ( ph -> ran H C_ dom F )
	cocan1g.4	|- ( ph -> Rel K )
	cocan1g.5	|- ( ph -> ran K C_ dom F )
Assertion	cocan1g	|- ( ph -> ( ( F o. H ) = ( F o. K ) <-> H = 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		cocan1g.4	|- ( ph -> Rel K )
5		cocan1g.5	|- ( ph -> ran K C_ dom F )
6	1 2 3	cocanss1	|- ( ph -> ( ( F o. H ) C_ ( F o. K ) <-> H C_ K ) )
7	1 4 5	cocanss1	|- ( ph -> ( ( F o. K ) C_ ( F o. H ) <-> K C_ H ) )
8	6 7	anbi12d	|- ( ph -> ( ( ( F o. H ) C_ ( F o. K ) /\ ( F o. K ) C_ ( F o. H ) ) <-> ( H C_ K /\ K C_ H ) ) )
9		eqss	|- ( ( F o. H ) = ( F o. K ) <-> ( ( F o. H ) C_ ( F o. K ) /\ ( F o. K ) C_ ( F o. H ) ) )
10		eqss	|- ( H = K <-> ( H C_ K /\ K C_ H ) )
11	8 9 10	3bitr4g	|- ( ph -> ( ( F o. H ) = ( F o. K ) <-> H = K ) )