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	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 𝐵 ) )
2		sotrieq	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) → ( 𝑥 = 𝐵 ↔ ¬ ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) ) )
3	2	necon2abid	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) ↔ 𝑥 ≠ 𝐵 ) )
4	3	anass1rs	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) ↔ 𝑥 ≠ 𝐵 ) )
5		breldmg	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝑥 𝑅 𝐵 ) → 𝑥 ∈ dom 𝑅 )
6	5	3expia	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 𝑅 𝐵 → 𝑥 ∈ dom 𝑅 ) )
7	6	ancoms	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝐵 → 𝑥 ∈ dom 𝑅 ) )
8		brelrng	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝐵 𝑅 𝑥 ) → 𝑥 ∈ ran 𝑅 )
9	8	3expia	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 𝑅 𝑥 → 𝑥 ∈ ran 𝑅 ) )
10	7 9	orim12d	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) → ( 𝑥 ∈ dom 𝑅 ∨ 𝑥 ∈ ran 𝑅 ) ) )
11		elun	⊢ ( 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ↔ ( 𝑥 ∈ dom 𝑅 ∨ 𝑥 ∈ ran 𝑅 ) )
12	10 11	imbitrrdi	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
13	12	adantll	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝐵 ∨ 𝐵 𝑅 𝑥 ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
14	4 13	sylbird	⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≠ 𝐵 → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
15	14	expimpd	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 𝐵 ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
16	1 15	biimtrid	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝐴 ∖ { 𝐵 } ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) ) )
17	16	ssrdv	⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝐵 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )