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

Metamath Proof Explorer

Theorem relresfld

Description: Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012)

Ref Expression
Assertion relresfld 
|- ( Rel R -> ( R |` U. U. R ) = R )

Proof

Step Hyp Ref Expression
1 relfld 
 |-  ( Rel R -> U. U. R = ( dom R u. ran R ) )
2 1 reseq2d 
 |-  ( Rel R -> ( R |` U. U. R ) = ( R |` ( dom R u. ran R ) ) )
3 resundi 
 |-  ( R |` ( dom R u. ran R ) ) = ( ( R |` dom R ) u. ( R |` ran R ) )
4 eqtr 
 |-  ( ( ( R |` U. U. R ) = ( R |` ( dom R u. ran R ) ) /\ ( R |` ( dom R u. ran R ) ) = ( ( R |` dom R ) u. ( R |` ran R ) ) ) -> ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) )
5 resss 
 |-  ( R |` ran R ) C_ R
6 resdm 
 |-  ( Rel R -> ( R |` dom R ) = R )
7 ssequn2 
 |-  ( ( R |` ran R ) C_ R <-> ( R u. ( R |` ran R ) ) = R )
8 uneq1 
 |-  ( ( R |` dom R ) = R -> ( ( R |` dom R ) u. ( R |` ran R ) ) = ( R u. ( R |` ran R ) ) )
9 8 eqeq2d 
 |-  ( ( R |` dom R ) = R -> ( ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) <-> ( R |` U. U. R ) = ( R u. ( R |` ran R ) ) ) )
10 eqtr 
 |-  ( ( ( R |` U. U. R ) = ( R u. ( R |` ran R ) ) /\ ( R u. ( R |` ran R ) ) = R ) -> ( R |` U. U. R ) = R )
11 10 ex 
 |-  ( ( R |` U. U. R ) = ( R u. ( R |` ran R ) ) -> ( ( R u. ( R |` ran R ) ) = R -> ( R |` U. U. R ) = R ) )
12 9 11 biimtrdi 
 |-  ( ( R |` dom R ) = R -> ( ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) -> ( ( R u. ( R |` ran R ) ) = R -> ( R |` U. U. R ) = R ) ) )
13 12 com3r 
 |-  ( ( R u. ( R |` ran R ) ) = R -> ( ( R |` dom R ) = R -> ( ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) -> ( R |` U. U. R ) = R ) ) )
14 7 13 sylbi 
 |-  ( ( R |` ran R ) C_ R -> ( ( R |` dom R ) = R -> ( ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) -> ( R |` U. U. R ) = R ) ) )
15 5 6 14 mpsyl 
 |-  ( Rel R -> ( ( R |` U. U. R ) = ( ( R |` dom R ) u. ( R |` ran R ) ) -> ( R |` U. U. R ) = R ) )
16 4 15 syl5com 
 |-  ( ( ( R |` U. U. R ) = ( R |` ( dom R u. ran R ) ) /\ ( R |` ( dom R u. ran R ) ) = ( ( R |` dom R ) u. ( R |` ran R ) ) ) -> ( Rel R -> ( R |` U. U. R ) = R ) )
17 2 3 16 sylancl 
 |-  ( Rel R -> ( Rel R -> ( R |` U. U. R ) = R ) )
18 17 pm2.43i 
 |-  ( Rel R -> ( R |` U. U. R ) = R )