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

Metamath Proof Explorer

Theorem tsrss

Description: Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 21-Nov-2013)

Ref Expression
Assertion tsrss ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ TosetRel )

Proof

Step Hyp Ref Expression
1 psss ⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )
2 inss1 ⊢ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅
3 dmss ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅 → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ dom 𝑅 )
4 ssralv ⊢ ( dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ dom 𝑅 → ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
5 2 3 4 mp2b ⊢ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
6 ssralv ⊢ ( dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ dom 𝑅 → ( ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
7 2 3 6 mp2b ⊢ ( ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
8 7 ralimi ⊢ ( ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
9 5 8 syl ⊢ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
10 inss2 ⊢ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
11 dmss ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ dom ( 𝐴 × 𝐴 ) )
12 10 11 ax-mp ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ dom ( 𝐴 × 𝐴 )
13 dmxpid ⊢ dom ( 𝐴 × 𝐴 ) = 𝐴
14 12 13 sseqtri ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝐴
15 14 sseli ⊢ ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) → 𝑥 ∈ 𝐴 )
16 14 sseli ⊢ ( 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) → 𝑦 ∈ 𝐴 )
17 brinxp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
18 brinxp ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
19 18 ancoms ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
20 17 19 orbi12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
21 15 16 20 syl2an ⊢ ( ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → ( ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
22 21 ralbidva ⊢ ( 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) → ( ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
23 22 ralbiia ⊢ ( ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
24 9 23 sylib ⊢ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
25 1 24 anim12i ⊢ ( ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ∧ ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
26 eqid ⊢ dom 𝑅 = dom 𝑅
27 26 istsr2 ⊢ ( 𝑅 ∈ TosetRel ↔ ( 𝑅 ∈ PosetRel ∧ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ dom 𝑅 ( 𝑥 𝑅 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
28 eqid ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) )
29 28 istsr2 ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ TosetRel ↔ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ∧ ∀ 𝑥 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∀ 𝑦 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∨ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
30 25 27 29 3imtr4i ⊢ ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ TosetRel )