Theorem dmcoss 5911

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 2143 and ax-12 2179. (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 1869	. . . . . 6 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧)
2		vex 3438	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3438	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opelco 5809	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		breq2 5093	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧))
6	5	cbvexvw 2038	. . . . . 6 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧)
7	1, 4, 6	3imtr4i 292	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
8	7	eximi 1836	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦∃𝑦 𝑥𝐵𝑦)
9	5	exexw 2053	. . . 4 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦∃𝑦 𝑥𝐵𝑦)
10	8, 9	sylibr 234	. . 3 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
11	2	eldm2 5839	. . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵))
12	2	eldm 5838	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
13	10, 11, 12	3imtr4i 292	. 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵)
14	13	ssriv 3936	1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵

Syntax hints:   ∧ wa 395  ∃wex 1780   ∈ wcel 2110   ⊆ wss 3900  ⟨cop 4580   class class class wbr 5089  dom cdm 5614   ∘ ccom 5618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-co 5623  df-dm 5624

This theorem is referenced by:  rncoss  5913  dmcosseq  5914  dmcosseqOLD  5915  dmcosseqOLDOLD  5916  cossxp  6215  fvco4i  6918  cofunexg  7876  fin23lem30  10225  wunco  10616  relexpnndm  14940  mvdco  19350  f1omvdconj  19351  znleval  21484  ofco2  22359  tngtopn  24558  xppreima  32617  cycpmrn  33102  relexp0a  43728  dmtrclfvRP  43742  dmtposss  48886