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 ) )