Theorem coexg

Description: The composition of two sets is a set. (Contributed by NM, 19-Mar-1998)

	Ref	Expression
Assertion	coexg	$$⊢\left(A\in V\wedge B\in W\right)\to A\circ B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		cossxp	$$⊢A\circ B\subseteq \mathrm{dom}B\times \mathrm{ran}A$$
2		dmexg	$$⊢B\in W\to \mathrm{dom}B\in \mathrm{V}$$
3		rnexg	$$⊢A\in V\to \mathrm{ran}A\in \mathrm{V}$$
4		xpexg	$$⊢\left(\mathrm{dom}B\in \mathrm{V}\wedge \mathrm{ran}A\in \mathrm{V}\right)\to \mathrm{dom}B\times \mathrm{ran}A\in \mathrm{V}$$
5	2 3 4	syl2anr	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{dom}B\times \mathrm{ran}A\in \mathrm{V}$$
6		ssexg	$$⊢\left(A\circ B\subseteq \mathrm{dom}B\times \mathrm{ran}A\wedge \mathrm{dom}B\times \mathrm{ran}A\in \mathrm{V}\right)\to A\circ B\in \mathrm{V}$$
7	1 5 6	sylancr	$$⊢\left(A\in V\wedge B\in W\right)\to A\circ B\in \mathrm{V}$$