Metamath Proof Explorer

Theorem psdmrn

Description: The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008)

Ref Expression
Assertion psdmrn 
|- ( R e. PosetRel -> ( dom R = U. U. R /\ ran 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. PosetRel -> dom R C_ U. U. R )
5 pslem 
 |-  ( R e. PosetRel -> ( ( ( x R x /\ x R x ) -> x R x ) /\ ( x e. U. U. R -> x R x ) /\ ( ( x R x /\ x R x ) -> x = x ) ) )
6 5 simp2d 
 |-  ( R e. PosetRel -> ( x e. U. U. R -> x R x ) )
7 vex 
 |-  x e. _V
8 7 7 breldm 
 |-  ( x R x -> x e. dom R )
9 6 8 syl6 
 |-  ( R e. PosetRel -> ( x e. U. U. R -> x e. dom R ) )
10 9 ssrdv 
 |-  ( R e. PosetRel -> U. U. R C_ dom R )
11 4 10 eqssd 
 |-  ( R e. PosetRel -> dom R = U. U. R )
12 ssun2 
 |-  ran R C_ ( dom R u. ran R )
13 12 2 sstri 
 |-  ran R C_ U. U. R
14 13 a1i 
 |-  ( R e. PosetRel -> ran R C_ U. U. R )
15 7 7 brelrn 
 |-  ( x R x -> x e. ran R )
16 6 15 syl6 
 |-  ( R e. PosetRel -> ( x e. U. U. R -> x e. ran R ) )
17 16 ssrdv 
 |-  ( R e. PosetRel -> U. U. R C_ ran R )
18 14 17 eqssd 
 |-  ( R e. PosetRel -> ran R = U. U. R )
19 11 18 jca 
 |-  ( R e. PosetRel -> ( dom R = U. U. R /\ ran R = U. U. R ) )