This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-10 and ax-12 . (Revised by TM, 31-Dec-2025)

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

Proof

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