Theorem dmrnssfld

Description: The domain and range of a class are included in its double union. (Contributed by NM, 13-May-2008)

	Ref	Expression
Assertion	dmrnssfld	$$⊢\mathrm{dom}A\cup \mathrm{ran}A\subseteq \bigcup \bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	eldm2	$$⊢x\in \mathrm{dom}A\leftrightarrow \exists y⟨x,y⟩\in A$$
3	1	prid1	$$⊢x\in \left\{x,y\right\}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	1 4	uniop	$$⊢\bigcup ⟨x,y⟩=\left\{x,y\right\}$$
6	1 4	uniopel	$$⊢⟨x,y⟩\in A\to \bigcup ⟨x,y⟩\in \bigcup A$$
7	5 6	eqeltrrid	$$⊢⟨x,y⟩\in A\to \left\{x,y\right\}\in \bigcup A$$
8		elssuni	$$⊢\left\{x,y\right\}\in \bigcup A\to \left\{x,y\right\}\subseteq \bigcup \bigcup A$$
9	7 8	syl	$$⊢⟨x,y⟩\in A\to \left\{x,y\right\}\subseteq \bigcup \bigcup A$$
10	9	sseld	$$⊢⟨x,y⟩\in A\to \left(x\in \left\{x,y\right\}\to x\in \bigcup \bigcup A\right)$$
11	3 10	mpi	$$⊢⟨x,y⟩\in A\to x\in \bigcup \bigcup A$$
12	11	exlimiv	$$⊢\exists y⟨x,y⟩\in A\to x\in \bigcup \bigcup A$$
13	2 12	sylbi	$$⊢x\in \mathrm{dom}A\to x\in \bigcup \bigcup A$$
14	13	ssriv	$$⊢\mathrm{dom}A\subseteq \bigcup \bigcup A$$
15	4	elrn2	$$⊢y\in \mathrm{ran}A\leftrightarrow \exists x⟨x,y⟩\in A$$
16	4	prid2	$$⊢y\in \left\{x,y\right\}$$
17	9	sseld	$$⊢⟨x,y⟩\in A\to \left(y\in \left\{x,y\right\}\to y\in \bigcup \bigcup A\right)$$
18	16 17	mpi	$$⊢⟨x,y⟩\in A\to y\in \bigcup \bigcup A$$
19	18	exlimiv	$$⊢\exists x⟨x,y⟩\in A\to y\in \bigcup \bigcup A$$
20	15 19	sylbi	$$⊢y\in \mathrm{ran}A\to y\in \bigcup \bigcup A$$
21	20	ssriv	$$⊢\mathrm{ran}A\subseteq \bigcup \bigcup A$$
22	14 21	unssi	$$⊢\mathrm{dom}A\cup \mathrm{ran}A\subseteq \bigcup \bigcup A$$