Theorem marypha2lem1

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

	Ref	Expression
Hypothesis	marypha2lem.t	$$⊢T=\bigcup _{x\in A}\left(\left\{x\right\}\times F\left(x\right)\right)$$
Assertion	marypha2lem1	$$⊢T\subseteq A\times \bigcup \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	$$⊢T=\bigcup _{x\in A}\left(\left\{x\right\}\times F\left(x\right)\right)$$
2		iunss	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times F\left(x\right)\right)\subseteq A\times \bigcup \mathrm{ran}F\leftrightarrow \forall x\in A\left\{x\right\}\times F\left(x\right)\subseteq A\times \bigcup \mathrm{ran}F$$
3		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
4		fvssunirn	$$⊢F\left(x\right)\subseteq \bigcup \mathrm{ran}F$$
5		xpss12	$$⊢\left(\left\{x\right\}\subseteq A\wedge F\left(x\right)\subseteq \bigcup \mathrm{ran}F\right)\to \left\{x\right\}\times F\left(x\right)\subseteq A\times \bigcup \mathrm{ran}F$$
6	3 4 5	sylancl	$$⊢x\in A\to \left\{x\right\}\times F\left(x\right)\subseteq A\times \bigcup \mathrm{ran}F$$
7	2 6	mprgbir	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times F\left(x\right)\right)\subseteq A\times \bigcup \mathrm{ran}F$$
8	1 7	eqsstri	$$⊢T\subseteq A\times \bigcup \mathrm{ran}F$$