Theorem dmcoss 5957

Description: Domain of a composition. Theorem 21 of [Suppes] p. 63. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) Avoid ax-10 2178 and ax-12 2213. (Revised by TM, 31-Dec-2025.)

Assertion

Ref	Expression
dmcoss	⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵

Proof of Theorem dmcoss

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

Step	Hyp	Ref	Expression
1		exsimpl 1901	. . . . . 6 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧)
2		vex 3455	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3455	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opelco 5849	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		breq2 5107	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧))
6	5	cbvexvw 2070	. . . . . 6 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧)
7	1, 4, 6	3imtr4i 295	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
8	7	eximi 1868	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦∃𝑦 𝑥𝐵𝑦)
9	5	exexw 2086	. . . 4 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦∃𝑦 𝑥𝐵𝑦)
10	8, 9	sylibr 237	. . 3 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
11	2	eldm2 5883	. . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵))
12	2	eldm 5882	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
13	10, 11, 12	3imtr4i 295	. 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵)
14	13	ssriv 3935	1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103  dom cdm 5651   ∘ ccom 5655

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-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-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-co 5660  df-dm 5661

This theorem is used by:  rncoss  5959  dmcosseq  5960  dmcosseqOLD  5961  cossxp  6267  fvco4i  6979  cofunexg  7950  fin23lem30  10401  wunco  10799  relexpnndm  15174  mvdco  19639  f1omvdconj  19640  znleval  21840  ofco2  22746  tngtopn  24949  xppreima  33221  cycpmrn  33686  relexp0a  44675  dmtrclfvRP  44689  dmtposss  49928