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	⊢ ( 𝜑 → Fun ◡ 𝐹 )
	cocan1g.2	⊢ ( 𝜑 → Rel 𝐻 )
	cocan1g.3	⊢ ( 𝜑 → ran 𝐻 ⊆ dom 𝐹 )
	cocan1g.4	⊢ ( 𝜑 → Rel 𝐾 )
	cocan1g.5	⊢ ( 𝜑 → ran 𝐾 ⊆ dom 𝐹 )
Assertion	cocan1g	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		cocan1g.1	⊢ ( 𝜑 → Fun ◡ 𝐹 )
2		cocan1g.2	⊢ ( 𝜑 → Rel 𝐻 )
3		cocan1g.3	⊢ ( 𝜑 → ran 𝐻 ⊆ dom 𝐹 )
4		cocan1g.4	⊢ ( 𝜑 → Rel 𝐾 )
5		cocan1g.5	⊢ ( 𝜑 → ran 𝐾 ⊆ dom 𝐹 )
6	1 2 3	cocanss1	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 ⊆ 𝐾 ) )
7	1 4 5	cocanss1	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐾 ) ⊆ ( 𝐹 ∘ 𝐻 ) ↔ 𝐾 ⊆ 𝐻 ) )
8	6 7	anbi12d	⊢ ( 𝜑 → ( ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ∧ ( 𝐹 ∘ 𝐾 ) ⊆ ( 𝐹 ∘ 𝐻 ) ) ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝐾 ⊆ 𝐻 ) ) )
9		eqss	⊢ ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ∧ ( 𝐹 ∘ 𝐾 ) ⊆ ( 𝐹 ∘ 𝐻 ) ) )
10		eqss	⊢ ( 𝐻 = 𝐾 ↔ ( 𝐻 ⊆ 𝐾 ∧ 𝐾 ⊆ 𝐻 ) )
11	8 9 10	3bitr4g	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) = ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 = 𝐾 ) )