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

Proof

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