Theorem dmcoss 5920

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 2142 and ax-12 2178. (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 1868	. . . . . 6 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧)
2		vex 3442	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3442	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opelco 5818	. . . . . 6 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		breq2 5099	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑥𝐵𝑦 ↔ 𝑥𝐵𝑧))
6	5	cbvexvw 2037	. . . . . 6 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧)
7	1, 4, 6	3imtr4i 292	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
8	7	eximi 1835	. . . 4 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦∃𝑦 𝑥𝐵𝑦)
9	5	exexw 2052	. . . 4 ⊢ (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑦∃𝑦 𝑥𝐵𝑦)
10	8, 9	sylibr 234	. . 3 ⊢ (∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵) → ∃𝑦 𝑥𝐵𝑦)
11	2	eldm2 5848	. . 3 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ 𝐵))
12	2	eldm 5847	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
13	10, 11, 12	3imtr4i 292	. 2 ⊢ (𝑥 ∈ dom (𝐴 ∘ 𝐵) → 𝑥 ∈ dom 𝐵)
14	13	ssriv 3941	1 ⊢ dom (𝐴 ∘ 𝐵) ⊆ dom 𝐵

Syntax hints:   ∧ wa 395  ∃wex 1779   ∈ wcel 2109   ⊆ wss 3905  ⟨cop 4585   class class class wbr 5095  dom cdm 5623   ∘ ccom 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-co 5632  df-dm 5633

This theorem is referenced by:  rncoss  5922  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  cossxp  6224  fvco4i  6928  cofunexg  7891  fin23lem30  10255  wunco  10646  relexpnndm  14966  mvdco  19342  f1omvdconj  19343  znleval  21479  ofco2  22354  tngtopn  24554  xppreima  32602  cycpmrn  33098  relexp0a  43689  dmtrclfvRP  43703  dmtposss  48848