Theorem relfld

Description: The double union of a relation is its field. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	relfld	|- ( Rel R -> U. U. R = ( dom R u. ran R ) )

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
2		uniss	|- ( R C_ ( dom R X. ran R ) -> U. R C_ U. ( dom R X. ran R ) )
3		uniss	|- ( U. R C_ U. ( dom R X. ran R ) -> U. U. R C_ U. U. ( dom R X. ran R ) )
4	1 2 3	3syl	|- ( Rel R -> U. U. R C_ U. U. ( dom R X. ran R ) )
5		unixpss	|- U. U. ( dom R X. ran R ) C_ ( dom R u. ran R )
6	4 5	sstrdi	|- ( Rel R -> U. U. R C_ ( dom R u. ran R ) )
7		dmrnssfld	|- ( dom R u. ran R ) C_ U. U. R
8	7	a1i	|- ( Rel R -> ( dom R u. ran R ) C_ U. U. R )
9	6 8	eqssd	|- ( Rel R -> U. U. R = ( dom R u. ran R ) )