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

Theorem dmcoss 5113
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  ( A  o.  B )  C_ 
dom  B

Proof of Theorem dmcoss
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfe1 1894 . . . 4  |-  F/ y E. y  x B y
2 exsimpl 1723 . . . . 5  |-  ( E. z ( x B z  /\  z A y )  ->  E. z  x B z )
3 vex 3083 . . . . . 6  |-  x  e. 
_V
4 vex 3083 . . . . . 6  |-  y  e. 
_V
53, 4opelco 5025 . . . . 5  |-  ( <.
x ,  y >.  e.  ( A  o.  B
)  <->  E. z ( x B z  /\  z A y ) )
6 breq2 4427 . . . . . 6  |-  ( y  =  z  ->  (
x B y  <->  x B
z ) )
76cbvexv 2082 . . . . 5  |-  ( E. y  x B y  <->  E. z  x B
z )
82, 5, 73imtr4i 269 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  B
)  ->  E. y  x B y )
91, 8exlimi 1972 . . 3  |-  ( E. y <. x ,  y
>.  e.  ( A  o.  B )  ->  E. y  x B y )
103eldm2 5052 . . 3  |-  ( x  e.  dom  ( A  o.  B )  <->  E. y <. x ,  y >.  e.  ( A  o.  B
) )
113eldm 5051 . . 3  |-  ( x  e.  dom  B  <->  E. y  x B y )
129, 10, 113imtr4i 269 . 2  |-  ( x  e.  dom  ( A  o.  B )  ->  x  e.  dom  B )
1312ssriv 3468 1  |-  dom  ( A  o.  B )  C_ 
dom  B
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370   E.wex 1657    e. wcel 1872    C_ wss 3436   <.cop 4004   class class class wbr 4423   dom cdm 4853    o. ccom 4857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-co 4862  df-dm 4863
This theorem is referenced by:  rncoss  5114  dmcosseq  5115  cossxp  5377  fvco4i  5960  cofunexg  6772  fin23lem30  8780  wunco  9166  relexpnndm  13105  mvdco  17086  f1omvdconj  17087  znleval  19124  ofco2  19475  tngtopn  21657  xppreima  28251  relexp0a  36279  dmtrclfvRP  36293
  Copyright terms: Public domain W3C validator