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

Metamath Proof Explorer

Theorem sofld

Description: The base set of a nonempty strict order is the same as the field of the relation. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion sofld ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 = ( dom 𝑅 ∪ ran 𝑅 ) )

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ( 𝐴 × 𝐴 )
2 relss ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ( Rel ( 𝐴 × 𝐴 ) → Rel 𝑅 ) )
3 1 2 mpi ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → Rel 𝑅 )
4 3 ad2antlr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → Rel 𝑅 )
5 df-br ⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
6 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑥 } )
7 undif1 ⊢ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) = ( 𝐴 ∪ { 𝑥 } )
8 6 7 sseqtrri ⊢ 𝐴 ⊆ ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } )
9 simpll ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑅 Or 𝐴 )
10 dmss ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → dom 𝑅 ⊆ dom ( 𝐴 × 𝐴 ) )
11 dmxpid ⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
12 10 11 sseqtrdi ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → dom 𝑅 ⊆ 𝐴 )
13 12 ad2antlr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → dom 𝑅 ⊆ 𝐴 )
14 3 ad2antlr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → Rel 𝑅 )
15 releldm ⊢ ( ( Rel 𝑅 ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
16 14 15 sylancom ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ dom 𝑅 )
17 13 16 sseldd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ 𝐴 )
18 sossfld ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
19 9 17 18 syl2anc ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( 𝐴 ∖ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
20 ssun1 ⊢ dom 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
21 20 16 sselid ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝑥 ∈ ( dom 𝑅 ∪ ran 𝑅 ) )
22 21 snssd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → { 𝑥 } ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
23 19 22 unssd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( ( 𝐴 ∖ { 𝑥 } ) ∪ { 𝑥 } ) ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
24 8 23 sstrid ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
25 24 ex ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
26 5 25 biimtrrid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
27 26 con3dimp ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
28 27 pm2.21d ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
29 4 28 relssdv ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝑅 ⊆ ∅ )
30 ss0 ⊢ ( 𝑅 ⊆ ∅ → 𝑅 = ∅ )
31 29 30 syl ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) ∧ ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) → 𝑅 = ∅ )
32 31 ex ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( ¬ 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) → 𝑅 = ∅ ) )
33 32 necon1ad ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ) → ( 𝑅 ≠ ∅ → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) ) )
34 33 3impia ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 ⊆ ( dom 𝑅 ∪ ran 𝑅 ) )
35 rnss ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ran 𝑅 ⊆ ran ( 𝐴 × 𝐴 ) )
36 rnxpid ⊢ ran ( 𝐴 × 𝐴 ) = 𝐴
37 35 36 sseqtrdi ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ran 𝑅 ⊆ 𝐴 )
38 12 37 unssd ⊢ ( 𝑅 ⊆ ( 𝐴 × 𝐴 ) → ( dom 𝑅 ∪ ran 𝑅 ) ⊆ 𝐴 )
39 38 3ad2ant2 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → ( dom 𝑅 ∪ ran 𝑅 ) ⊆ 𝐴 )
40 34 39 eqssd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ⊆ ( 𝐴 × 𝐴 ) ∧ 𝑅 ≠ ∅ ) → 𝐴 = ( dom 𝑅 ∪ ran 𝑅 ) )