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 \land B \in A) \to A ∖ \{B\} \subseteq dom R \cup ran R$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ x \in (A ∖ \{B\}) \leftrightarrow (x \in A \land x \neq B)$
2		sotrieq	$⊢ (R Or A \land (x \in A \land B \in A)) \to (x = B \leftrightarrow \neg (x R B \lor B R x))$
3	2	necon2abid	$⊢ (R Or A \land (x \in A \land B \in A)) \to ((x R B \lor B R x) \leftrightarrow x \neq B)$
4	3	anass1rs	$⊢ ((R Or A \land B \in A) \land x \in A) \to ((x R B \lor B R x) \leftrightarrow x \neq B)$
5		breldmg	$⊢ (x \in A \land B \in A \land x R B) \to x \in dom R$
6	5	3expia	$⊢ (x \in A \land B \in A) \to (x R B \to x \in dom R)$
7	6	ancoms	$⊢ (B \in A \land x \in A) \to (x R B \to x \in dom R)$
8		brelrng	$⊢ (B \in A \land x \in A \land B R x) \to x \in ran R$
9	8	3expia	$⊢ (B \in A \land x \in A) \to (B R x \to x \in ran R)$
10	7 9	orim12d	$⊢ (B \in A \land x \in A) \to ((x R B \lor B R x) \to (x \in dom R \lor x \in ran R))$
11		elun	$⊢ x \in (dom R \cup ran R) \leftrightarrow (x \in dom R \lor x \in ran R)$
12	10 11	imbitrrdi	$⊢ (B \in A \land x \in A) \to ((x R B \lor B R x) \to x \in (dom R \cup ran R))$
13	12	adantll	$⊢ ((R Or A \land B \in A) \land x \in A) \to ((x R B \lor B R x) \to x \in (dom R \cup ran R))$
14	4 13	sylbird	$⊢ ((R Or A \land B \in A) \land x \in A) \to (x \neq B \to x \in (dom R \cup ran R))$
15	14	expimpd	$⊢ (R Or A \land B \in A) \to ((x \in A \land x \neq B) \to x \in (dom R \cup ran R))$
16	1 15	biimtrid	$⊢ (R Or A \land B \in A) \to (x \in (A ∖ \{B\}) \to x \in (dom R \cup ran R))$
17	16	ssrdv	$⊢ (R Or A \land B \in A) \to A ∖ \{B\} \subseteq dom R \cup ran R$