Metamath Proof Explorer

Theorem dirdm

Description: A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

Ref Expression
Assertion dirdm 
|- ( R e. DirRel -> dom R = U. U. R )

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  dom R C_ ( dom R u. ran R )
2 dmrnssfld 
 |-  ( dom R u. ran R ) C_ U. U. R
3 1 2 sstri 
 |-  dom R C_ U. U. R
4 3 a1i 
 |-  ( R e. DirRel -> dom R C_ U. U. R )
5 dmresi 
 |-  dom ( _I |` U. U. R ) = U. U. R
6 eqid 
 |-  U. U. R = U. U. R
7 6 isdir 
 |-  ( R e. DirRel -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) ) )
8 7 ibi 
 |-  ( R e. DirRel -> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) )
9 8 simplrd 
 |-  ( R e. DirRel -> ( _I |` U. U. R ) C_ R )
10 dmss 
 |-  ( ( _I |` U. U. R ) C_ R -> dom ( _I |` U. U. R ) C_ dom R )
11 9 10 syl 
 |-  ( R e. DirRel -> dom ( _I |` U. U. R ) C_ dom R )
12 5 11 eqsstrrid 
 |-  ( R e. DirRel -> U. U. R C_ dom R )
13 4 12 eqssd 
 |-  ( R e. DirRel -> dom R = U. U. R )