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