This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )