Theorem cocanss2

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

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

Proof

Step	Hyp	Ref	Expression
1		cocan2g.1	⊢ ( 𝜑 → Fun 𝐹 )
2		cocan2g.2	⊢ ( 𝜑 → Rel 𝐻 )
3		cocan2g.3	⊢ ( 𝜑 → dom 𝐻 ⊆ ran 𝐹 )
4	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → Rel 𝐻 )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑧 ∈ V
7	5 6	breldm	⊢ ( 𝑦 𝐻 𝑧 → 𝑦 ∈ dom 𝐻 )
8	3	sseld	⊢ ( 𝜑 → ( 𝑦 ∈ dom 𝐻 → 𝑦 ∈ ran 𝐹 ) )
9	7 8	syl5	⊢ ( 𝜑 → ( 𝑦 𝐻 𝑧 → 𝑦 ∈ ran 𝐹 ) )
10	5	elrn	⊢ ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 𝑥 𝐹 𝑦 )
11	9 10	imbitrdi	⊢ ( 𝜑 → ( 𝑦 𝐻 𝑧 → ∃ 𝑥 𝑥 𝐹 𝑦 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( 𝑦 𝐻 𝑧 → ∃ 𝑥 𝑥 𝐹 𝑦 ) )
13		19.8a	⊢ ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → ∃ 𝑦 ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) )
14		vex	⊢ 𝑥 ∈ V
15	14 6	brco	⊢ ( 𝑥 ( 𝐻 ∘ 𝐹 ) 𝑧 ↔ ∃ 𝑦 ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) )
16	13 15	sylibr	⊢ ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → 𝑥 ( 𝐻 ∘ 𝐹 ) 𝑧 )
17		ssbr	⊢ ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → ( 𝑥 ( 𝐻 ∘ 𝐹 ) 𝑧 → 𝑥 ( 𝐾 ∘ 𝐹 ) 𝑧 ) )
18	16 17	syl5	⊢ ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → 𝑥 ( 𝐾 ∘ 𝐹 ) 𝑧 ) )
19	14 6	brco	⊢ ( 𝑥 ( 𝐾 ∘ 𝐹 ) 𝑧 ↔ ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) )
20	18 19	imbitrdi	⊢ ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) ) )
22		vex	⊢ 𝑤 ∈ V
23	14 5 22	fununiq	⊢ ( Fun 𝐹 → ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑤 ) → 𝑦 = 𝑤 ) )
24	23	imp	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑤 ) ) → 𝑦 = 𝑤 )
25	24	breq1d	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑤 ) ) → ( 𝑦 𝐾 𝑧 ↔ 𝑤 𝐾 𝑧 ) )
26	25	biimprd	⊢ ( ( Fun 𝐹 ∧ ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑤 ) ) → ( 𝑤 𝐾 𝑧 → 𝑦 𝐾 𝑧 ) )
27	26	expr	⊢ ( ( Fun 𝐹 ∧ 𝑥 𝐹 𝑦 ) → ( 𝑥 𝐹 𝑤 → ( 𝑤 𝐾 𝑧 → 𝑦 𝐾 𝑧 ) ) )
28	27	impd	⊢ ( ( Fun 𝐹 ∧ 𝑥 𝐹 𝑦 ) → ( ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) )
29	28	exlimdv	⊢ ( ( Fun 𝐹 ∧ 𝑥 𝐹 𝑦 ) → ( ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) )
30	1 29	sylan	⊢ ( ( 𝜑 ∧ 𝑥 𝐹 𝑦 ) → ( ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) )
31	30	ex	⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 → ( ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( 𝑥 𝐹 𝑦 → ( ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) ) )
33	32	adantrd	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → ( ∃ 𝑤 ( 𝑥 𝐹 𝑤 ∧ 𝑤 𝐾 𝑧 ) → 𝑦 𝐾 𝑧 ) ) )
34	21 33	mpdd	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( ( 𝑥 𝐹 𝑦 ∧ 𝑦 𝐻 𝑧 ) → 𝑦 𝐾 𝑧 ) )
35	34	expd	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( 𝑥 𝐹 𝑦 → ( 𝑦 𝐻 𝑧 → 𝑦 𝐾 𝑧 ) ) )
36	35	exlimdv	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( ∃ 𝑥 𝑥 𝐹 𝑦 → ( 𝑦 𝐻 𝑧 → 𝑦 𝐾 𝑧 ) ) )
37	36	com23	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( 𝑦 𝐻 𝑧 → ( ∃ 𝑥 𝑥 𝐹 𝑦 → 𝑦 𝐾 𝑧 ) ) )
38	12 37	mpdd	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( 𝑦 𝐻 𝑧 → 𝑦 𝐾 𝑧 ) )
39		df-br	⊢ ( 𝑦 𝐻 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐻 )
40		df-br	⊢ ( 𝑦 𝐾 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐾 )
41	38 39 40	3imtr3g	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐻 → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐾 ) )
42	4 41	relssdv	⊢ ( ( 𝜑 ∧ ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ) → 𝐻 ⊆ 𝐾 )
43	42	ex	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) → 𝐻 ⊆ 𝐾 ) )
44		coss1	⊢ ( 𝐻 ⊆ 𝐾 → ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) )
45	43 44	impbid1	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ⊆ ( 𝐾 ∘ 𝐹 ) ↔ 𝐻 ⊆ 𝐾 ) )