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

Metamath Proof Explorer

Theorem sossfld

Description: The base set of a strict order is contained in the field of the relation, except possibly for one element (note that (/) Or { B } ). (Contributed by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion sossfld 
|- ( ( R Or A /\ B e. A ) -> ( A \ { B } ) C_ ( dom R u. ran R ) )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( x e. ( A \ { B } ) <-> ( x e. A /\ x =/= B ) )
2 sotrieq 
 |-  ( ( R Or A /\ ( x e. A /\ B e. A ) ) -> ( x = B <-> -. ( x R B \/ B R x ) ) )
3 2 necon2abid 
 |-  ( ( R Or A /\ ( x e. A /\ B e. A ) ) -> ( ( x R B \/ B R x ) <-> x =/= B ) )
4 3 anass1rs 
 |-  ( ( ( R Or A /\ B e. A ) /\ x e. A ) -> ( ( x R B \/ B R x ) <-> x =/= B ) )
5 breldmg 
 |-  ( ( x e. A /\ B e. A /\ x R B ) -> x e. dom R )
6 5 3expia 
 |-  ( ( x e. A /\ B e. A ) -> ( x R B -> x e. dom R ) )
7 6 ancoms 
 |-  ( ( B e. A /\ x e. A ) -> ( x R B -> x e. dom R ) )
8 brelrng 
 |-  ( ( B e. A /\ x e. A /\ B R x ) -> x e. ran R )
9 8 3expia 
 |-  ( ( B e. A /\ x e. A ) -> ( B R x -> x e. ran R ) )
10 7 9 orim12d 
 |-  ( ( B e. A /\ x e. A ) -> ( ( x R B \/ B R x ) -> ( x e. dom R \/ x e. ran R ) ) )
11 elun 
 |-  ( x e. ( dom R u. ran R ) <-> ( x e. dom R \/ x e. ran R ) )
12 10 11 imbitrrdi 
 |-  ( ( B e. A /\ x e. A ) -> ( ( x R B \/ B R x ) -> x e. ( dom R u. ran R ) ) )
13 12 adantll 
 |-  ( ( ( R Or A /\ B e. A ) /\ x e. A ) -> ( ( x R B \/ B R x ) -> x e. ( dom R u. ran R ) ) )
14 4 13 sylbird 
 |-  ( ( ( R Or A /\ B e. A ) /\ x e. A ) -> ( x =/= B -> x e. ( dom R u. ran R ) ) )
15 14 expimpd 
 |-  ( ( R Or A /\ B e. A ) -> ( ( x e. A /\ x =/= B ) -> x e. ( dom R u. ran R ) ) )
16 1 15 biimtrid 
 |-  ( ( R Or A /\ B e. A ) -> ( x e. ( A \ { B } ) -> x e. ( dom R u. ran R ) ) )
17 16 ssrdv 
 |-  ( ( R Or A /\ B e. A ) -> ( A \ { B } ) C_ ( dom R u. ran R ) )