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

Theorem dmcoss 4943
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 1707 . . . 4  |-  F/ y E. y  x B y
2 exsimpl 1579 . . . . 5  |-  ( E. z ( x B z  /\  z A y )  ->  E. z  x B z )
3 vex 2792 . . . . . 6  |-  x  e. 
_V
4 vex 2792 . . . . . 6  |-  y  e. 
_V
53, 4opelco 4852 . . . . 5  |-  ( <.
x ,  y >.  e.  ( A  o.  B
)  <->  E. z ( x B z  /\  z A y ) )
6 breq2 4028 . . . . . 6  |-  ( y  =  z  ->  (
x B y  <->  x B
z ) )
76cbvexv 1948 . . . . 5  |-  ( E. y  x B y  <->  E. z  x B
z )
82, 5, 73imtr4i 257 . . . 4  |-  ( <.
x ,  y >.  e.  ( A  o.  B
)  ->  E. y  x B y )
91, 8exlimi 1803 . . 3  |-  ( E. y <. x ,  y
>.  e.  ( A  o.  B )  ->  E. y  x B y )
103eldm2 4876 . . 3  |-  ( x  e.  dom  (  A  o.  B )  <->  E. y <. x ,  y >.  e.  ( A  o.  B
) )
113eldm 4875 . . 3  |-  ( x  e.  dom  B  <->  E. y  x B y )
129, 10, 113imtr4i 257 . 2  |-  ( x  e.  dom  (  A  o.  B )  ->  x  e.  dom  B )
1312ssriv 3185 1  |-  dom  (  A  o.  B )  C_ 
dom  B
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528    e. wcel 1685    C_ wss 3153   <.cop 3644   class class class wbr 4024    dom cdm 4688    o. ccom 4692
This theorem is referenced by:  rncoss  4944  dmcosseq  4945  cossxp  5193  coexg  5213  fvco4i  5559  cofunexg  5701  fin23lem30  7964  wunco  8351  znleval  16504  tngtopn  18162  relexpdm  23439  mvdco  26799  f1omvdconj  26800
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-opab 4079  df-co 4697  df-dm 4698
  Copyright terms: Public domain W3C validator