Theorem tsrdir

Description: A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Assertion	tsrdir	⊢ ( 𝐴 ∈ TosetRel → 𝐴 ∈ DirRel )

Proof

Step	Hyp	Ref	Expression
1		tsrps	⊢ ( 𝐴 ∈ TosetRel → 𝐴 ∈ PosetRel )
2		psrel	⊢ ( 𝐴 ∈ PosetRel → Rel 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ TosetRel → Rel 𝐴 )
4		psref2	⊢ ( 𝐴 ∈ PosetRel → ( 𝐴 ∩ ◡ 𝐴 ) = ( I ↾ ∪ ∪ 𝐴 ) )
5		inss1	⊢ ( 𝐴 ∩ ◡ 𝐴 ) ⊆ 𝐴
6	4 5	eqsstrrdi	⊢ ( 𝐴 ∈ PosetRel → ( I ↾ ∪ ∪ 𝐴 ) ⊆ 𝐴 )
7	1 6	syl	⊢ ( 𝐴 ∈ TosetRel → ( I ↾ ∪ ∪ 𝐴 ) ⊆ 𝐴 )
8	3 7	jca	⊢ ( 𝐴 ∈ TosetRel → ( Rel 𝐴 ∧ ( I ↾ ∪ ∪ 𝐴 ) ⊆ 𝐴 ) )
9		pstr2	⊢ ( 𝐴 ∈ PosetRel → ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 )
10	1 9	syl	⊢ ( 𝐴 ∈ TosetRel → ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 )
11		psdmrn	⊢ ( 𝐴 ∈ PosetRel → ( dom 𝐴 = ∪ ∪ 𝐴 ∧ ran 𝐴 = ∪ ∪ 𝐴 ) )
12	1 11	syl	⊢ ( 𝐴 ∈ TosetRel → ( dom 𝐴 = ∪ ∪ 𝐴 ∧ ran 𝐴 = ∪ ∪ 𝐴 ) )
13	12	simpld	⊢ ( 𝐴 ∈ TosetRel → dom 𝐴 = ∪ ∪ 𝐴 )
14	13	sqxpeqd	⊢ ( 𝐴 ∈ TosetRel → ( dom 𝐴 × dom 𝐴 ) = ( ∪ ∪ 𝐴 × ∪ ∪ 𝐴 ) )
15		eqid	⊢ dom 𝐴 = dom 𝐴
16	15	istsr	⊢ ( 𝐴 ∈ TosetRel ↔ ( 𝐴 ∈ PosetRel ∧ ( dom 𝐴 × dom 𝐴 ) ⊆ ( 𝐴 ∪ ◡ 𝐴 ) ) )
17	16	simprbi	⊢ ( 𝐴 ∈ TosetRel → ( dom 𝐴 × dom 𝐴 ) ⊆ ( 𝐴 ∪ ◡ 𝐴 ) )
18		relcoi2	⊢ ( Rel 𝐴 → ( ( I ↾ ∪ ∪ 𝐴 ) ∘ 𝐴 ) = 𝐴 )
19	3 18	syl	⊢ ( 𝐴 ∈ TosetRel → ( ( I ↾ ∪ ∪ 𝐴 ) ∘ 𝐴 ) = 𝐴 )
20		cnvresid	⊢ ◡ ( I ↾ ∪ ∪ 𝐴 ) = ( I ↾ ∪ ∪ 𝐴 )
21		cnvss	⊢ ( ( I ↾ ∪ ∪ 𝐴 ) ⊆ 𝐴 → ◡ ( I ↾ ∪ ∪ 𝐴 ) ⊆ ◡ 𝐴 )
22	7 21	syl	⊢ ( 𝐴 ∈ TosetRel → ◡ ( I ↾ ∪ ∪ 𝐴 ) ⊆ ◡ 𝐴 )
23	20 22	eqsstrrid	⊢ ( 𝐴 ∈ TosetRel → ( I ↾ ∪ ∪ 𝐴 ) ⊆ ◡ 𝐴 )
24		coss1	⊢ ( ( I ↾ ∪ ∪ 𝐴 ) ⊆ ◡ 𝐴 → ( ( I ↾ ∪ ∪ 𝐴 ) ∘ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
25	23 24	syl	⊢ ( 𝐴 ∈ TosetRel → ( ( I ↾ ∪ ∪ 𝐴 ) ∘ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
26	19 25	eqsstrrd	⊢ ( 𝐴 ∈ TosetRel → 𝐴 ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
27		relcnv	⊢ Rel ◡ 𝐴
28		relcoi1	⊢ ( Rel ◡ 𝐴 → ( ◡ 𝐴 ∘ ( I ↾ ∪ ∪ ◡ 𝐴 ) ) = ◡ 𝐴 )
29	27 28	ax-mp	⊢ ( ◡ 𝐴 ∘ ( I ↾ ∪ ∪ ◡ 𝐴 ) ) = ◡ 𝐴
30		relcnvfld	⊢ ( Rel 𝐴 → ∪ ∪ 𝐴 = ∪ ∪ ◡ 𝐴 )
31	3 30	syl	⊢ ( 𝐴 ∈ TosetRel → ∪ ∪ 𝐴 = ∪ ∪ ◡ 𝐴 )
32	31	reseq2d	⊢ ( 𝐴 ∈ TosetRel → ( I ↾ ∪ ∪ 𝐴 ) = ( I ↾ ∪ ∪ ◡ 𝐴 ) )
33	32 7	eqsstrrd	⊢ ( 𝐴 ∈ TosetRel → ( I ↾ ∪ ∪ ◡ 𝐴 ) ⊆ 𝐴 )
34		coss2	⊢ ( ( I ↾ ∪ ∪ ◡ 𝐴 ) ⊆ 𝐴 → ( ◡ 𝐴 ∘ ( I ↾ ∪ ∪ ◡ 𝐴 ) ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
35	33 34	syl	⊢ ( 𝐴 ∈ TosetRel → ( ◡ 𝐴 ∘ ( I ↾ ∪ ∪ ◡ 𝐴 ) ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
36	29 35	eqsstrrid	⊢ ( 𝐴 ∈ TosetRel → ◡ 𝐴 ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
37	26 36	unssd	⊢ ( 𝐴 ∈ TosetRel → ( 𝐴 ∪ ◡ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
38	17 37	sstrd	⊢ ( 𝐴 ∈ TosetRel → ( dom 𝐴 × dom 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
39	14 38	eqsstrrd	⊢ ( 𝐴 ∈ TosetRel → ( ∪ ∪ 𝐴 × ∪ ∪ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) )
40	10 39	jca	⊢ ( 𝐴 ∈ TosetRel → ( ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ∧ ( ∪ ∪ 𝐴 × ∪ ∪ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) ) )
41		eqid	⊢ ∪ ∪ 𝐴 = ∪ ∪ 𝐴
42	41	isdir	⊢ ( 𝐴 ∈ TosetRel → ( 𝐴 ∈ DirRel ↔ ( ( Rel 𝐴 ∧ ( I ↾ ∪ ∪ 𝐴 ) ⊆ 𝐴 ) ∧ ( ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ∧ ( ∪ ∪ 𝐴 × ∪ ∪ 𝐴 ) ⊆ ( ◡ 𝐴 ∘ 𝐴 ) ) ) ) )
43	8 40 42	mpbir2and	⊢ ( 𝐴 ∈ TosetRel → 𝐴 ∈ DirRel )