Theorem cocanss2 46058

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 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
4		vex 3454	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
5	3, 4	breldm 5891	. . . . . . . . 9 ⊢ (𝑦𝐻𝑧 → 𝑦 ∈ dom 𝐻)
6		cocan2g.3	. . . . . . . . . 10 ⊢ (𝜑 → dom 𝐻 ⊆ ran 𝐹)
7	6	sseld 3908	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 ∈ dom 𝐻 → 𝑦 ∈ ran 𝐹))
8	5, 7	syl5 35	. . . . . . . 8 ⊢ (𝜑 → (𝑦𝐻𝑧 → 𝑦 ∈ ran 𝐹))
9	3	elrn 5876	. . . . . . . 8 ⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 𝑥𝐹𝑦)
10	8, 9	imbitrdi 254	. . . . . . 7 ⊢ (𝜑 → (𝑦𝐻𝑧 → ∃𝑥 𝑥𝐹𝑦))
11	10	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → ∃𝑥 𝑥𝐹𝑦))
12		19.8a 2217	. . . . . . . . . . . . . 14 ⊢ ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑦(𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧))
13		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
14	13, 4	brco 5849	. . . . . . . . . . . . . 14 ⊢ (𝑥(𝐻 ∘ 𝐹)𝑧 ↔ ∃𝑦(𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧))
15	12, 14	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → 𝑥(𝐻 ∘ 𝐹)𝑧)
16		ssbr 5148	. . . . . . . . . . . . 13 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → (𝑥(𝐻 ∘ 𝐹)𝑧 → 𝑥(𝐾 ∘ 𝐹)𝑧))
17	15, 16	syl5 35	. . . . . . . . . . . 12 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → 𝑥(𝐾 ∘ 𝐹)𝑧))
18	13, 4	brco 5849	. . . . . . . . . . . 12 ⊢ (𝑥(𝐾 ∘ 𝐹)𝑧 ↔ ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧))
19	17, 18	imbitrdi 254	. . . . . . . . . . 11 ⊢ ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧)))
20	19	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → ((𝑥𝐹𝑦 ∧ 𝑦𝐻𝑧) → ∃𝑤(𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧)))
21		cocan2g.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Fun 𝐹)
22		vex 3454	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑤 ∈ V
23	13, 3, 22	fununiq 6560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Fun 𝐹 → ((𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤) → 𝑦 = 𝑤))
24	23	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → 𝑦 = 𝑤)
25	24	breq1d 5112	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → (𝑦𝐾𝑧 ↔ 𝑤𝐾𝑧))
26	25	biimprd 251	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐹 ∧ (𝑥𝐹𝑦 ∧ 𝑥𝐹𝑤)) → (𝑤𝐾𝑧 → 𝑦𝐾𝑧))
27	26	expr 462	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐹 ∧ 𝑥𝐹𝑦) → (𝑥𝐹𝑤 → (𝑤𝐾𝑧 → 𝑦𝐾𝑧)))
28	27	impd 416	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐹 ∧ 𝑥𝐹𝑦) → ((𝑥𝐹𝑤 ∧ 𝑤𝐾𝑧) → 𝑦𝐾𝑧))
29	28	exlimdv 1965	. . . . . . . . . . . . . 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 1965	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (∃𝑥 𝑥𝐹𝑦 → (𝑦𝐻𝑧 → 𝑦𝐾𝑧)))
37	36	com23 87	. . . . . 6 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → (∃𝑥 𝑥𝐹𝑦 → 𝑦𝐾𝑧)))
38	11, 37	mpdd 44	. . . . 5 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (𝑦𝐻𝑧 → 𝑦𝐾𝑧))
39		df-br 5103	. . . . 5 ⊢ (𝑦𝐻𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐻)
40		df-br 5103	. . . . 5 ⊢ (𝑦𝐾𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐾)
41	38, 39, 40	3imtr3g 298	. . . 4 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → (⟨𝑦, 𝑧⟩ ∈ 𝐻 → ⟨𝑦, 𝑧⟩ ∈ 𝐾))
42	2, 41	relssdv 5765	. . 3 ⊢ ((𝜑 ∧ (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹)) → 𝐻 ⊆ 𝐾)
43	42	ex 418	. 2 ⊢ (𝜑 → ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) → 𝐻 ⊆ 𝐾))
44		coss1 5834	. 2 ⊢ (𝐻 ⊆ 𝐾 → (𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹))
45	43, 44	impbid1 228	1 ⊢ (𝜑 → ((𝐻 ∘ 𝐹) ⊆ (𝐾 ∘ 𝐹) ↔ 𝐻 ⊆ 𝐾))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2144   ⊆ wss 3896  ⟨cop 4834   class class class wbr 5102  dom cdm 5651  ran crn 5652   ∘ ccom 5655  Rel wrel 5656  Fun wfun 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6545

This theorem is used by:  cocan2g  46059  cocanss1  46060