Metamath Proof Explorer

Theorem sofld

Description: The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion sofld 
|- ( ( R Or A /\ R C_ ( A X. A ) /\ R =/= (/) ) -> A = ( dom R u. ran R ) )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. A )
2 relss 
 |-  ( R C_ ( A X. A ) -> ( Rel ( A X. A ) -> Rel R ) )
3 1 2 mpi 
 |-  ( R C_ ( A X. A ) -> Rel R )
4 3 ad2antlr 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ -. A C_ ( dom R u. ran R ) ) -> Rel R )
5 df-br 
 |-  ( x R y <-> <. x , y >. e. R )
6 ssun1 
 |-  A C_ ( A u. { x } )
7 undif1 
 |-  ( ( A \ { x } ) u. { x } ) = ( A u. { x } )
8 6 7 sseqtrri 
 |-  A C_ ( ( A \ { x } ) u. { x } )
9 simpll 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> R Or A )
10 dmss 
 |-  ( R C_ ( A X. A ) -> dom R C_ dom ( A X. A ) )
11 dmxpid 
 |-  dom ( A X. A ) = A
12 10 11 sseqtrdi 
 |-  ( R C_ ( A X. A ) -> dom R C_ A )
13 12 ad2antlr 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> dom R C_ A )
14 3 ad2antlr 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> Rel R )
15 releldm 
 |-  ( ( Rel R /\ x R y ) -> x e. dom R )
16 14 15 sylancom 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> x e. dom R )
17 13 16 sseldd 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> x e. A )
18 sossfld 
 |-  ( ( R Or A /\ x e. A ) -> ( A \ { x } ) C_ ( dom R u. ran R ) )
19 9 17 18 syl2anc 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> ( A \ { x } ) C_ ( dom R u. ran R ) )
20 ssun1 
 |-  dom R C_ ( dom R u. ran R )
21 20 16 sseldi 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> x e. ( dom R u. ran R ) )
22 21 snssd 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> { x } C_ ( dom R u. ran R ) )
23 19 22 unssd 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> ( ( A \ { x } ) u. { x } ) C_ ( dom R u. ran R ) )
24 8 23 sstrid 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ x R y ) -> A C_ ( dom R u. ran R ) )
25 24 ex 
 |-  ( ( R Or A /\ R C_ ( A X. A ) ) -> ( x R y -> A C_ ( dom R u. ran R ) ) )
26 5 25 syl5bir 
 |-  ( ( R Or A /\ R C_ ( A X. A ) ) -> ( <. x , y >. e. R -> A C_ ( dom R u. ran R ) ) )
27 26 con3dimp 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ -. A C_ ( dom R u. ran R ) ) -> -. <. x , y >. e. R )
28 27 pm2.21d 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ -. A C_ ( dom R u. ran R ) ) -> ( <. x , y >. e. R -> <. x , y >. e. (/) ) )
29 4 28 relssdv 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ -. A C_ ( dom R u. ran R ) ) -> R C_ (/) )
30 ss0 
 |-  ( R C_ (/) -> R = (/) )
31 29 30 syl 
 |-  ( ( ( R Or A /\ R C_ ( A X. A ) ) /\ -. A C_ ( dom R u. ran R ) ) -> R = (/) )
32 31 ex 
 |-  ( ( R Or A /\ R C_ ( A X. A ) ) -> ( -. A C_ ( dom R u. ran R ) -> R = (/) ) )
33 32 necon1ad 
 |-  ( ( R Or A /\ R C_ ( A X. A ) ) -> ( R =/= (/) -> A C_ ( dom R u. ran R ) ) )
34 33 3impia 
 |-  ( ( R Or A /\ R C_ ( A X. A ) /\ R =/= (/) ) -> A C_ ( dom R u. ran R ) )
35 rnss 
 |-  ( R C_ ( A X. A ) -> ran R C_ ran ( A X. A ) )
36 rnxpid 
 |-  ran ( A X. A ) = A
37 35 36 sseqtrdi 
 |-  ( R C_ ( A X. A ) -> ran R C_ A )
38 12 37 unssd 
 |-  ( R C_ ( A X. A ) -> ( dom R u. ran R ) C_ A )
39 38 3ad2ant2 
 |-  ( ( R Or A /\ R C_ ( A X. A ) /\ R =/= (/) ) -> ( dom R u. ran R ) C_ A )
40 34 39 eqssd 
 |-  ( ( R Or A /\ R C_ ( A X. A ) /\ R =/= (/) ) -> A = ( dom R u. ran R ) )