MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmcoss Structured version   Visualization version   GIF version

Theorem dmcoss 5984
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.)
Assertion
Ref Expression
dmcoss dom (𝐴𝐵) ⊆ dom 𝐵

Proof of Theorem dmcoss
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfe1 2149 . . . 4 𝑦𝑦 𝑥𝐵𝑦
2 exsimpl 1867 . . . . 5 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) → ∃𝑧 𝑥𝐵𝑧)
3 vex 3483 . . . . . 6 𝑥 ∈ V
4 vex 3483 . . . . . 6 𝑦 ∈ V
53, 4opelco 5881 . . . . 5 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
6 breq2 5146 . . . . . 6 (𝑦 = 𝑧 → (𝑥𝐵𝑦𝑥𝐵𝑧))
76cbvexvw 2035 . . . . 5 (∃𝑦 𝑥𝐵𝑦 ↔ ∃𝑧 𝑥𝐵𝑧)
82, 5, 73imtr4i 292 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴𝐵) → ∃𝑦 𝑥𝐵𝑦)
91, 8exlimi 2216 . . 3 (∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵) → ∃𝑦 𝑥𝐵𝑦)
103eldm2 5911 . . 3 (𝑥 ∈ dom (𝐴𝐵) ↔ ∃𝑦𝑥, 𝑦⟩ ∈ (𝐴𝐵))
113eldm 5910 . . 3 (𝑥 ∈ dom 𝐵 ↔ ∃𝑦 𝑥𝐵𝑦)
129, 10, 113imtr4i 292 . 2 (𝑥 ∈ dom (𝐴𝐵) → 𝑥 ∈ dom 𝐵)
1312ssriv 3986 1 dom (𝐴𝐵) ⊆ dom 𝐵
Colors of variables: wff setvar class
Syntax hints:  wa 395  wex 1778  wcel 2107  wss 3950  cop 4631   class class class wbr 5142  dom cdm 5684  ccom 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-co 5693  df-dm 5694
This theorem is referenced by:  rncoss  5985  dmcosseq  5986  dmcosseqOLD  5987  cossxp  6291  fvco4i  7009  cofunexg  7974  fin23lem30  10383  wunco  10774  relexpnndm  15081  mvdco  19464  f1omvdconj  19465  znleval  21574  ofco2  22458  tngtopn  24672  xppreima  32656  cycpmrn  33164  relexp0a  43734  dmtrclfvRP  43748  dmtposss  48782
  Copyright terms: Public domain W3C validator