Theorem cocanss1

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

	Ref	Expression
Hypotheses	cocan1g.1	⊢ ( 𝜑 → Fun ◡ 𝐹 )
	cocan1g.2	⊢ ( 𝜑 → Rel 𝐻 )
	cocan1g.3	⊢ ( 𝜑 → ran 𝐻 ⊆ dom 𝐹 )
Assertion	cocanss1	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 ⊆ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		cocan1g.1	⊢ ( 𝜑 → Fun ◡ 𝐹 )
2		cocan1g.2	⊢ ( 𝜑 → Rel 𝐻 )
3		cocan1g.3	⊢ ( 𝜑 → ran 𝐻 ⊆ dom 𝐹 )
4		relcnv	⊢ Rel ◡ 𝐻
5	4	a1i	⊢ ( 𝜑 → Rel ◡ 𝐻 )
6		df-rn	⊢ ran 𝐻 = dom ◡ 𝐻
7		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
8	3 6 7	3sstr3g	⊢ ( 𝜑 → dom ◡ 𝐻 ⊆ ran ◡ 𝐹 )
9	1 5 8	cocanss2	⊢ ( 𝜑 → ( ( ◡ 𝐻 ∘ ◡ 𝐹 ) ⊆ ( ◡ 𝐾 ∘ ◡ 𝐹 ) ↔ ◡ 𝐻 ⊆ ◡ 𝐾 ) )
10		relco	⊢ Rel ( 𝐹 ∘ 𝐻 )
11		cnvssb	⊢ ( Rel ( 𝐹 ∘ 𝐻 ) → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ◡ ( 𝐹 ∘ 𝐻 ) ⊆ ◡ ( 𝐹 ∘ 𝐾 ) ) )
12	10 11	ax-mp	⊢ ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ◡ ( 𝐹 ∘ 𝐻 ) ⊆ ◡ ( 𝐹 ∘ 𝐾 ) )
13		cnvco	⊢ ◡ ( 𝐹 ∘ 𝐻 ) = ( ◡ 𝐻 ∘ ◡ 𝐹 )
14		cnvco	⊢ ◡ ( 𝐹 ∘ 𝐾 ) = ( ◡ 𝐾 ∘ ◡ 𝐹 )
15	13 14	sseq12i	⊢ ( ◡ ( 𝐹 ∘ 𝐻 ) ⊆ ◡ ( 𝐹 ∘ 𝐾 ) ↔ ( ◡ 𝐻 ∘ ◡ 𝐹 ) ⊆ ( ◡ 𝐾 ∘ ◡ 𝐹 ) )
16	12 15	bitri	⊢ ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ( ◡ 𝐻 ∘ ◡ 𝐹 ) ⊆ ( ◡ 𝐾 ∘ ◡ 𝐹 ) )
17	16	a1i	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ ( ◡ 𝐻 ∘ ◡ 𝐹 ) ⊆ ( ◡ 𝐾 ∘ ◡ 𝐹 ) ) )
18		cnvssb	⊢ ( Rel 𝐻 → ( 𝐻 ⊆ 𝐾 ↔ ◡ 𝐻 ⊆ ◡ 𝐾 ) )
19	2 18	syl	⊢ ( 𝜑 → ( 𝐻 ⊆ 𝐾 ↔ ◡ 𝐻 ⊆ ◡ 𝐾 ) )
20	9 17 19	3bitr4d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ⊆ ( 𝐹 ∘ 𝐾 ) ↔ 𝐻 ⊆ 𝐾 ) )