# Metamath Proof Explorer

## 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 {ℝ}^{*}×{ℝ}^{*}$
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}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {y}\wedge {y}\le {z}\right)\to {x}\le {z}\right)$
14 13 gen2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {y}\wedge {y}\le {z}\right)\to {x}\le {z}\right)$
15 cotr ${⊢}\le \circ \le \subseteq \le ↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\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}↾}_{\bigcup \bigcup \le }↔\forall {x}\in \bigcup \bigcup \le \phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {y}\wedge {y}\le {x}\right)↔{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}↔\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}↔\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}↔{x}\le {y}\right)$
29 breq1 ${⊢}{x}={y}\to \left({x}\le {x}↔{y}\le {x}\right)$
30 28 29 anbi12d ${⊢}{x}={y}\to \left(\left({x}\le {x}\wedge {x}\le {x}\right)↔\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)↔{x}={y}\right)$
33 32 alrimiv ${⊢}{x}\in {ℝ}^{*}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {y}\wedge {y}\le {x}\right)↔{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}\phantom{\rule{.4em}{0ex}}\left(\left({x}\le {y}\wedge {y}\le {x}\right)↔{x}={y}\right)$
37 17 36 mprgbir ${⊢}\le \cap {\le }^{-1}={\mathrm{I}↾}_{\bigcup \bigcup \le }$
38 xrex ${⊢}{ℝ}^{*}\in \mathrm{V}$
39 38 38 xpex ${⊢}{ℝ}^{*}×{ℝ}^{*}\in \mathrm{V}$
40 39 2 ssexi ${⊢}\le \in \mathrm{V}$
41 isps ${⊢}\le \in \mathrm{V}\to \left(\le \in \mathrm{PosetRel}↔\left(\mathrm{Rel}\le \wedge \le \circ \le \subseteq \le \wedge \le \cap {\le }^{-1}={\mathrm{I}↾}_{\bigcup \bigcup \le }\right)\right)$
42 40 41 ax-mp ${⊢}\le \in \mathrm{PosetRel}↔\left(\mathrm{Rel}\le \wedge \le \circ \le \subseteq \le \wedge \le \cap {\le }^{-1}={\mathrm{I}↾}_{\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 {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\vee {y}\le {x}\right)$
46 qfto ${⊢}{ℝ}^{*}×{ℝ}^{*}\subseteq \le \cup {\le }^{-1}↔\forall {x}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{*}\phantom{\rule{.4em}{0ex}}\left({x}\le {y}\vee {y}\le {x}\right)$
47 45 46 mpbir ${⊢}{ℝ}^{*}×{ℝ}^{*}\subseteq \le \cup {\le }^{-1}$
48 ledm ${⊢}{ℝ}^{*}=\mathrm{dom}\le$
49 48 istsr ${⊢}\le \in \mathrm{TosetRel}↔\left(\le \in \mathrm{PosetRel}\wedge {ℝ}^{*}×{ℝ}^{*}\subseteq \le \cup {\le }^{-1}\right)$
50 43 47 49 mpbir2an ${⊢}\le \in \mathrm{TosetRel}$