Theorem dmcoss 5932

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 2147 and ax-12 2185. (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 1870	. . . . . 6 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧)
2		vex 3446	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3446	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opelco 5828	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		breq2 5104	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧))
6	5	cbvexvw 2039	. . . . . 6 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧)
7	1, 4, 6	3imtr4i 292	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
8	7	eximi 1837	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦∃𝑦 𝑥𝐵𝑦)
9	5	exexw 2055	. . . 4 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦∃𝑦 𝑥𝐵𝑦)
10	8, 9	sylibr 234	. . 3 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
11	2	eldm2 5858	. . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵))
12	2	eldm 5857	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
13	10, 11, 12	3imtr4i 292	. 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵)
14	13	ssriv 3939	1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵

Syntax hints:   ∧ wa 395  ∃wex 1781   ∈ wcel 2114   ⊆ wss 3903  ⟨cop 4588   class class class wbr 5100  dom cdm 5632   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-co 5641  df-dm 5642

This theorem is referenced by:  rncoss  5934  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  cossxp  6238  fvco4i  6943  cofunexg  7903  fin23lem30  10264  wunco  10656  relexpnndm  14976  mvdco  19386  f1omvdconj  19387  znleval  21521  ofco2  22407  tngtopn  24606  xppreima  32734  cycpmrn  33236  relexp0a  44061  dmtrclfvRP  44075  dmtposss  49224