Theorem dmcoss 5385

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.

Step	Hyp	Ref	Expression
1		nfe1 2027	. . . 4 |- F/ y E. y x B y
2		exsimpl 1795	. . . . 5 |- ( E. z ( x B z /\ z A y ) -> E. z x B z )
3		vex 3203	. . . . . 6 |- x e. _V
4		vex 3203	. . . . . 6 |- y e. _V
5	3, 4	opelco 5293	. . . . 5 |- ( <. x , y >. e. ( A o. B ) <-> E. z ( x B z /\ z A y ) )
6		breq2 4657	. . . . . 6 |- ( y = z -> ( x B y <-> x B z ) )
7	6	cbvexv 2275	. . . . 5 |- ( E. y x B y <-> E. z x B z )
8	2, 5, 7	3imtr4i 281	. . . 4 |- ( <. x , y >. e. ( A o. B ) -> E. y x B y )
9	1, 8	exlimi 2086	. . 3 |- ( E. y <. x , y >. e. ( A o. B ) -> E. y x B y )
10	3	eldm2 5322	. . 3 |- ( x e. dom ( A o. B ) <-> E. y <. x , y >. e. ( A o. B ) )
11	3	eldm 5321	. . 3 |- ( x e. dom B <-> E. y x B y )
12	9, 10, 11	3imtr4i 281	. 2 |- ( x e. dom ( A o. B ) -> x e. dom B )
13	12	ssriv 3607	1 |- dom ( A o. B ) C_ dom B

Syntax hints:   /\ wa 384   E.wex 1704   e. wcel 1990   C_ wss 3574   <.cop 4183   class class class wbr 4653   dom cdm 5114   o. ccom 5118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-co 5123  df-dm 5124

This theorem is referenced by:  rncoss  5386  dmcosseq  5387  cossxp  5658  fvco4i  6276  cofunexg  7130  fin23lem30  9164  wunco  9555  relexpnndm  13781  mvdco  17865  f1omvdconj  17866  znleval  19903  ofco2  20257  tngtopn  22454  xppreima  29449  relexp0a  38008  dmtrclfvRP  38022