Theorem djussxp

Description: Disjoint union is a subset of a Cartesian product. (Contributed by Stefan O'Rear, 21-Nov-2014)

	Ref	Expression
Assertion	djussxp	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\subseteq A\times \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		iunss	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\subseteq A\times \mathrm{V}\leftrightarrow \forall x\in A\left\{x\right\}\times B\subseteq A\times \mathrm{V}$$
2		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
3		ssv	$$⊢B\subseteq \mathrm{V}$$
4		xpss12	$$⊢\left(\left\{x\right\}\subseteq A\wedge B\subseteq \mathrm{V}\right)\to \left\{x\right\}\times B\subseteq A\times \mathrm{V}$$
5	2 3 4	sylancl	$$⊢x\in A\to \left\{x\right\}\times B\subseteq A\times \mathrm{V}$$
6	1 5	mprgbir	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)\subseteq A\times \mathrm{V}$$