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