Theorem cocanss2 45921

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

Hypotheses

Ref	Expression
cocan2g.1	⊢ (𝜑 → Fun 𝐹)
cocan2g.2	⊢ (𝜑 → Rel 𝐻)
cocan2g.3	⊢ (𝜑 → dom 𝐻 ⊆ ran 𝐹)

Assertion

Ref	Expression
cocanss2	⊢ (𝜑 → ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) ↔ 𝐻 ⊆ 𝐾))

Proof of Theorem cocanss2

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cocan2g.2	. . . . 5 ⊢ (𝜑 → Rel 𝐻)
2	1	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → Rel 𝐻)
3		vex 3455	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
4		vex 3455	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
5	3, 4	breldm 5890	. . . . . . . . 9 ⊢ (𝑦𝐻𝑧 → 𝑦 ∈ dom 𝐻)
6		cocan2g.3	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝐻 ⊆ ran 𝐹)
7	6	sseld 3930	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ dom 𝐻 → 𝑦 ∈ ran 𝐹))
8	5, 7	syl5 35	. . . . . . . 8 ⊢ (𝜑 → (𝑦𝐻𝑧 → 𝑦 ∈ ran 𝐹))
9	3	elrn 5875	. . . . . . . 8 ⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 𝑥𝐹𝑦)
10	8, 9	imbitrdi 254	. . . . . . 7 ⊢ (𝜑 → (𝑦𝐻𝑧 → ∃𝑥 𝑥𝐹𝑦))
11	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → ∃𝑥 𝑥𝐹𝑦))
12		19.8a 2218	. . . . . . . . . . . . . 14 ⊢ ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑦(𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧))
13		vex 3455	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
14	13, 4	brco 5848	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝐻 ∘ 𝐹)𝑧 ↔ ∃𝑦(𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧))
15	12, 14	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → 𝑥(𝐻 ∘ 𝐹)𝑧)
16		ssbr 5149	. . . . . . . . . . . . 13 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → (𝑥(𝐻 ∘ 𝐹)𝑧 → 𝑥(𝐾 ∘ 𝐹)𝑧))
17	15, 16	syl5 35	. . . . . . . . . . . 12 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → 𝑥(𝐾 ∘ 𝐹)𝑧))
18	13, 4	brco 5848	. . . . . . . . . . . 12 ⊢ (𝑥(𝐾 ∘ 𝐹)𝑧 ↔ ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧))
19	17, 18	imbitrdi 254	. . . . . . . . . . 11 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧)))
20	19	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧)))
21		cocan2g.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun 𝐹)
22		vex 3455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
23	13, 3, 22	fununiq 6555	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝐹 → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤) → 𝑦 = 𝑤))
24	23	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → 𝑦 = 𝑤)
25	24	breq1d 5113	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → (𝑦𝐾𝑧 ↔ 𝑤𝐾𝑧))
26	25	biimprd 251	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → (𝑤𝐾𝑧 → 𝑦𝐾𝑧))
27	26	expr 462	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑥𝐹𝑦) → (𝑥𝐹𝑤 → (𝑤𝐾𝑧 → 𝑦𝐾𝑧)))
28	27	impd 416	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑥𝐹𝑦) → ((𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧))
29	28	exlimdv 1966	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑥𝐹𝑦) → (∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧))
30	21, 29	sylan 592	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥𝐹𝑦) → (∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧))
31	30	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥𝐹𝑦 → (∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧)))
32	31	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑥𝐹𝑦 → (∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧)))
33	32	adantrd 497	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → (∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧)))
34	20, 33	mpdd 44	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → 𝑦𝐾𝑧))
35	34	expd 421	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑥𝐹𝑦 → (𝑦𝐻𝑧 → 𝑦𝐾𝑧)))
36	35	exlimdv 1966	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (∃𝑥 𝑥𝐹𝑦 → (𝑦𝐻𝑧 → 𝑦𝐾𝑧)))
37	36	com23 87	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → (∃𝑥 𝑥𝐹𝑦 → 𝑦𝐾𝑧)))
38	11, 37	mpdd 44	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → 𝑦𝐾𝑧))
39		df-br 5104	. . . . 5 ⊢ (𝑦𝐻𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐻)
40		df-br 5104	. . . . 5 ⊢ (𝑦𝐾𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐾)
41	38, 39, 40	3imtr3g 298	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (⟨𝑦, 𝑧⟩ ∈ 𝐻 → ⟨𝑦, 𝑧⟩ ∈ 𝐾))
42	2, 41	relssdv 5764	. . 3 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → 𝐻 ⊆ 𝐾)
43	42	ex 418	. 2 ⊢ (𝜑 → ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → 𝐻 ⊆ 𝐾))
44		coss1 5833	. 2 ⊢ (𝐻 ⊆ 𝐾 → (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹))
45	43, 44	impbid1 228	1 ⊢ (𝜑 → ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) ↔ 𝐻 ⊆ 𝐾))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103  dom cdm 5651  ran crn 5652   ∘ ccom 5655  Rel wrel 5656  Fun wfun 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6540

This theorem is used by:  cocan2g  45922  cocanss1  45923