Theorem letsr

Description: The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	letsr	$$⊢\le \in \mathrm{TosetRel}$$

Proof

Step	Hyp	Ref	Expression
1		lerel	$$⊢\mathrm{Rel}\le$$
2		lerelxr	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$
3	2	brel	$$⊢x\le y\to \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)$$
4	3	adantr	$$⊢\left(x\le y\wedge y\le z\right)\to \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)$$
5	4	simpld	$$⊢\left(x\le y\wedge y\le z\right)\to x\in {ℝ}^{*}$$
6	4	simprd	$$⊢\left(x\le y\wedge y\le z\right)\to y\in {ℝ}^{*}$$
7	2	brel	$$⊢y\le z\to \left(y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)$$
8	7	simprd	$$⊢y\le z\to z\in {ℝ}^{*}$$
9	8	adantl	$$⊢\left(x\le y\wedge y\le z\right)\to z\in {ℝ}^{*}$$
10	5 6 9	3jca	$$⊢\left(x\le y\wedge y\le z\right)\to \left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)$$
11		xrletr	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\to \left(\left(x\le y\wedge y\le z\right)\to x\le z\right)$$
12	10 11	mpcom	$$⊢\left(x\le y\wedge y\le z\right)\to x\le z$$
13	12	ax-gen	$$⊢\forall z\left(\left(x\le y\wedge y\le z\right)\to x\le z\right)$$
14	13	gen2	$$⊢\forall x\forall y\forall z\left(\left(x\le y\wedge y\le z\right)\to x\le z\right)$$
15		cotr	$$⊢\le \circ \le \subseteq \le \leftrightarrow \forall x\forall y\forall z\left(\left(x\le y\wedge y\le z\right)\to x\le z\right)$$
16	14 15	mpbir	$$⊢\le \circ \le \subseteq \le$$
17		asymref	$$⊢\le \cap {\le }^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup \le }\leftrightarrow \forall x\in \bigcup \bigcup \le \forall y\left(\left(x\le y\wedge y\le x\right)\leftrightarrow x=y\right)$$
18		simpr	$$⊢\left(x\in {ℝ}^{*}\wedge \left(x\le y\wedge y\le x\right)\right)\to \left(x\le y\wedge y\le x\right)$$
19	2	brel	$$⊢y\le x\to \left(y\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)$$
20	19	simpld	$$⊢y\le x\to y\in {ℝ}^{*}$$
21	20	adantl	$$⊢\left(x\le y\wedge y\le x\right)\to y\in {ℝ}^{*}$$
22		xrletri3	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x=y\leftrightarrow \left(x\le y\wedge y\le x\right)\right)$$
23	21 22	sylan2	$$⊢\left(x\in {ℝ}^{*}\wedge \left(x\le y\wedge y\le x\right)\right)\to \left(x=y\leftrightarrow \left(x\le y\wedge y\le x\right)\right)$$
24	18 23	mpbird	$$⊢\left(x\in {ℝ}^{*}\wedge \left(x\le y\wedge y\le x\right)\right)\to x=y$$
25	24	ex	$$⊢x\in {ℝ}^{*}\to \left(\left(x\le y\wedge y\le x\right)\to x=y\right)$$
26		xrleid	$$⊢x\in {ℝ}^{*}\to x\le x$$
27	26 26	jca	$$⊢x\in {ℝ}^{*}\to \left(x\le x\wedge x\le x\right)$$
28		breq2	$$⊢x=y\to \left(x\le x\leftrightarrow x\le y\right)$$
29		breq1	$$⊢x=y\to \left(x\le x\leftrightarrow y\le x\right)$$
30	28 29	anbi12d	$$⊢x=y\to \left(\left(x\le x\wedge x\le x\right)\leftrightarrow \left(x\le y\wedge y\le x\right)\right)$$
31	27 30	syl5ibcom	$$⊢x\in {ℝ}^{*}\to \left(x=y\to \left(x\le y\wedge y\le x\right)\right)$$
32	25 31	impbid	$$⊢x\in {ℝ}^{*}\to \left(\left(x\le y\wedge y\le x\right)\leftrightarrow x=y\right)$$
33	32	alrimiv	$$⊢x\in {ℝ}^{*}\to \forall y\left(\left(x\le y\wedge y\le x\right)\leftrightarrow x=y\right)$$
34		lefld	$$⊢{ℝ}^{*}=\bigcup \bigcup \le$$
35	34	eqcomi	$$⊢\bigcup \bigcup \le ={ℝ}^{*}$$
36	33 35	eleq2s	$$⊢x\in \bigcup \bigcup \le \to \forall y\left(\left(x\le y\wedge y\le x\right)\leftrightarrow x=y\right)$$
37	17 36	mprgbir	$$⊢\le \cap {\le }^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup \le }$$
38		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
39	38 38	xpex	$$⊢{ℝ}^{*}\times {ℝ}^{*}\in \mathrm{V}$$
40	39 2	ssexi	$$⊢\le \in \mathrm{V}$$
41		isps	$$⊢\le \in \mathrm{V}\to \left(\le \in \mathrm{PosetRel}\leftrightarrow \left(\mathrm{Rel}\le \wedge \le \circ \le \subseteq \le \wedge \le \cap {\le }^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup \le }\right)\right)$$
42	40 41	ax-mp	$$⊢\le \in \mathrm{PosetRel}\leftrightarrow \left(\mathrm{Rel}\le \wedge \le \circ \le \subseteq \le \wedge \le \cap {\le }^{-1}={\mathrm{I}\upharpoonright }_{\bigcup \bigcup \le }\right)$$
43	1 16 37 42	mpbir3an	$$⊢\le \in \mathrm{PosetRel}$$
44		xrletri	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left(x\le y\vee y\le x\right)$$
45	44	rgen2	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x\le y\vee y\le x\right)$$
46		qfto	$$⊢{ℝ}^{*}\times {ℝ}^{*}\subseteq \le \cup {\le }^{-1}\leftrightarrow \forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left(x\le y\vee y\le x\right)$$
47	45 46	mpbir	$$⊢{ℝ}^{*}\times {ℝ}^{*}\subseteq \le \cup {\le }^{-1}$$
48		ledm	$$⊢{ℝ}^{*}=\mathrm{dom}\le$$
49	48	istsr	$$⊢\le \in \mathrm{TosetRel}\leftrightarrow \left(\le \in \mathrm{PosetRel}\wedge {ℝ}^{*}\times {ℝ}^{*}\subseteq \le \cup {\le }^{-1}\right)$$
50	43 47 49	mpbir2an	$$⊢\le \in \mathrm{TosetRel}$$