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	|- ( dom A u. ran A ) C_ U. U. A

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	eldm2	|- ( x e. dom A <-> E. y <. x , y >. e. A )
3	1	prid1	|- x e. { x , y }
4		vex	|- y e. _V
5	1 4	uniop	|- U. <. x , y >. = { x , y }
6	1 4	uniopel	|- ( <. x , y >. e. A -> U. <. x , y >. e. U. A )
7	5 6	eqeltrrid	|- ( <. x , y >. e. A -> { x , y } e. U. A )
8		elssuni	|- ( { x , y } e. U. A -> { x , y } C_ U. U. A )
9	7 8	syl	|- ( <. x , y >. e. A -> { x , y } C_ U. U. A )
10	9	sseld	|- ( <. x , y >. e. A -> ( x e. { x , y } -> x e. U. U. A ) )
11	3 10	mpi	|- ( <. x , y >. e. A -> x e. U. U. A )
12	11	exlimiv	|- ( E. y <. x , y >. e. A -> x e. U. U. A )
13	2 12	sylbi	|- ( x e. dom A -> x e. U. U. A )
14	13	ssriv	|- dom A C_ U. U. A
15	4	elrn2	|- ( y e. ran A <-> E. x <. x , y >. e. A )
16	4	prid2	|- y e. { x , y }
17	9	sseld	|- ( <. x , y >. e. A -> ( y e. { x , y } -> y e. U. U. A ) )
18	16 17	mpi	|- ( <. x , y >. e. A -> y e. U. U. A )
19	18	exlimiv	|- ( E. x <. x , y >. e. A -> y e. U. U. A )
20	15 19	sylbi	|- ( y e. ran A -> y e. U. U. A )
21	20	ssriv	|- ran A C_ U. U. A
22	14 21	unssi	|- ( dom A u. ran A ) C_ U. U. A