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	$$⊢A\in \mathrm{TosetRel}\to A\in \mathrm{DirRel}$$

Proof

Step	Hyp	Ref	Expression
1		tsrps	$$⊢A\in \mathrm{TosetRel}\to A\in \mathrm{PosetRel}$$
2		psrel	$$⊢A\in \mathrm{PosetRel}\to \mathrm{Rel}A$$
3	1 2	syl	$$⊢A\in \mathrm{TosetRel}\to \mathrm{Rel}A$$
4		psref2	$$⊢A\in \mathrm{PosetRel}\to A\cap A^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}$$
5		inss1	$$⊢A\cap A^{-1}\subseteq A$$
6	4 5	eqsstrrdi	$$⊢A\in \mathrm{PosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A$$
7	1 6	syl	$$⊢A\in \mathrm{TosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A$$
8	3 7	jca	$$⊢A\in \mathrm{TosetRel}\to \left(\mathrm{Rel}A\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A\right)$$
9		pstr2	$$⊢A\in \mathrm{PosetRel}\to A\circ A\subseteq A$$
10	1 9	syl	$$⊢A\in \mathrm{TosetRel}\to A\circ A\subseteq A$$
11		psdmrn	$$⊢A\in \mathrm{PosetRel}\to \left(\mathrm{dom}A=\bigcup \bigcup A\wedge \mathrm{ran}A=\bigcup \bigcup A\right)$$
12	1 11	syl	$$⊢A\in \mathrm{TosetRel}\to \left(\mathrm{dom}A=\bigcup \bigcup A\wedge \mathrm{ran}A=\bigcup \bigcup A\right)$$
13	12	simpld	$$⊢A\in \mathrm{TosetRel}\to \mathrm{dom}A=\bigcup \bigcup A$$
14	13	sqxpeqd	$$⊢A\in \mathrm{TosetRel}\to \mathrm{dom}A\times \mathrm{dom}A=\bigcup \bigcup A\times \bigcup \bigcup A$$
15		eqid	$$⊢\mathrm{dom}A=\mathrm{dom}A$$
16	15	istsr	$$⊢A\in \mathrm{TosetRel}\leftrightarrow \left(A\in \mathrm{PosetRel}\wedge \mathrm{dom}A\times \mathrm{dom}A\subseteq A\cup A^{-1}\right)$$
17	16	simprbi	$$⊢A\in \mathrm{TosetRel}\to \mathrm{dom}A\times \mathrm{dom}A\subseteq A\cup A^{-1}$$
18		relcoi2	$$⊢\mathrm{Rel}A\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)\circ A=A$$
19	3 18	syl	$$⊢A\in \mathrm{TosetRel}\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)\circ A=A$$
20		cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)}^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}$$
21		cnvss	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A\to {\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)}^{-1}\subseteq A^{-1}$$
22	7 21	syl	$$⊢A\in \mathrm{TosetRel}\to {\left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)}^{-1}\subseteq A^{-1}$$
23	20 22	eqsstrrid	$$⊢A\in \mathrm{TosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A^{-1}$$
24		coss1	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A^{-1}\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)\circ A\subseteq A^{-1}\circ A$$
25	23 24	syl	$$⊢A\in \mathrm{TosetRel}\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\right)\circ A\subseteq A^{-1}\circ A$$
26	19 25	eqsstrrd	$$⊢A\in \mathrm{TosetRel}\to A\subseteq A^{-1}\circ A$$
27		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
28		relcoi1	$$⊢\mathrm{Rel}{A}^{-1}\to A^{-1}\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\right)=A^{-1}$$
29	27 28	ax-mp	$$⊢A^{-1}\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\right)=A^{-1}$$
30		relcnvfld	$$⊢\mathrm{Rel}A\to \bigcup \bigcup A=\bigcup \bigcup A^{-1}$$
31	3 30	syl	$$⊢A\in \mathrm{TosetRel}\to \bigcup \bigcup A=\bigcup \bigcup A^{-1}$$
32	31	reseq2d	$$⊢A\in \mathrm{TosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}$$
33	32 7	eqsstrrd	$$⊢A\in \mathrm{TosetRel}\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\subseteq A$$
34		coss2	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\subseteq A\to A^{-1}\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\right)\subseteq A^{-1}\circ A$$
35	33 34	syl	$$⊢A\in \mathrm{TosetRel}\to A^{-1}\circ \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup A^{-1}}\right)\subseteq A^{-1}\circ A$$
36	29 35	eqsstrrid	$$⊢A\in \mathrm{TosetRel}\to A^{-1}\subseteq A^{-1}\circ A$$
37	26 36	unssd	$$⊢A\in \mathrm{TosetRel}\to A\cup A^{-1}\subseteq A^{-1}\circ A$$
38	17 37	sstrd	$$⊢A\in \mathrm{TosetRel}\to \mathrm{dom}A\times \mathrm{dom}A\subseteq A^{-1}\circ A$$
39	14 38	eqsstrrd	$$⊢A\in \mathrm{TosetRel}\to \bigcup \bigcup A\times \bigcup \bigcup A\subseteq A^{-1}\circ A$$
40	10 39	jca	$$⊢A\in \mathrm{TosetRel}\to \left(A\circ A\subseteq A\wedge \bigcup \bigcup A\times \bigcup \bigcup A\subseteq A^{-1}\circ A\right)$$
41		eqid	$$⊢\bigcup \bigcup A=\bigcup \bigcup A$$
42	41	isdir	$$⊢A\in \mathrm{TosetRel}\to \left(A\in \mathrm{DirRel}\leftrightarrow \left(\left(\mathrm{Rel}A\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup A}\subseteq A\right)\wedge \left(A\circ A\subseteq A\wedge \bigcup \bigcup A\times \bigcup \bigcup A\subseteq A^{-1}\circ A\right)\right)\right)$$
43	8 40 42	mpbir2and	$$⊢A\in \mathrm{TosetRel}\to A\in \mathrm{DirRel}$$