Metamath Proof Explorer

Theorem dmcoss

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)

Ref Expression
Assertion dmcoss 
|- dom ( A o. B ) C_ dom B

Proof

Step Hyp Ref Expression
1 nfe1 
 |-  F/ y E. y x B y
2 exsimpl 
 |-  ( E. z ( x B z /\ z A y ) -> E. z x B z )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 opelco 
 |-  ( <. x , y >. e. ( A o. B ) <-> E. z ( x B z /\ z A y ) )
6 breq2 
 |-  ( y = z -> ( x B y <-> x B z ) )
7 6 cbvexvw 
 |-  ( E. y x B y <-> E. z x B z )
8 2 5 7 3imtr4i 
 |-  ( <. x , y >. e. ( A o. B ) -> E. y x B y )
9 1 8 exlimi 
 |-  ( E. y <. x , y >. e. ( A o. B ) -> E. y x B y )
10 3 eldm2 
 |-  ( x e. dom ( A o. B ) <-> E. y <. x , y >. e. ( A o. B ) )
11 3 eldm 
 |-  ( x e. dom B <-> E. y x B y )
12 9 10 11 3imtr4i 
 |-  ( x e. dom ( A o. B ) -> x e. dom B )
13 12 ssriv 
 |-  dom ( A o. B ) C_ dom B