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	$$⊢\mathrm{dom}\left(A\circ B\right)\subseteq \mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		nfe1	$$⊢Ⅎy\exists yxBy$$
2		exsimpl	$$⊢\exists z\left(xBz\wedge zAy\right)\to \exists zxBz$$
3		vex	$$⊢x\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	opelco	$$⊢⟨x,y⟩\in \left(A\circ B\right)\leftrightarrow \exists z\left(xBz\wedge zAy\right)$$
6		breq2	$$⊢y=z\to \left(xBy\leftrightarrow xBz\right)$$
7	6	cbvexvw	$$⊢\exists yxBy\leftrightarrow \exists zxBz$$
8	2 5 7	3imtr4i	$$⊢⟨x,y⟩\in \left(A\circ B\right)\to \exists yxBy$$
9	1 8	exlimi	$$⊢\exists y⟨x,y⟩\in \left(A\circ B\right)\to \exists yxBy$$
10	3	eldm2	$$⊢x\in \mathrm{dom}\left(A\circ B\right)\leftrightarrow \exists y⟨x,y⟩\in \left(A\circ B\right)$$
11	3	eldm	$$⊢x\in \mathrm{dom}B\leftrightarrow \exists yxBy$$
12	9 10 11	3imtr4i	$$⊢x\in \mathrm{dom}\left(A\circ B\right)\to x\in \mathrm{dom}B$$
13	12	ssriv	$$⊢\mathrm{dom}\left(A\circ B\right)\subseteq \mathrm{dom}B$$