Theorem letsr 18226

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.)

Assertion

Ref	Expression
letsr	⊢ ≤ ∈ TosetRel

Proof of Theorem letsr

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lerel 10970	. . 3 ⊢ Rel ≤
2		lerelxr 10969	. . . . . . . . . . 11 ⊢ ≤ ⊆ (ℝ* × ℝ*)
3	2	brel 5643	. . . . . . . . . 10 ⊢ (𝑥 ≤ 𝑦 → (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
4	3	adantr 480	. . . . . . . . 9 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*))
5	4	simpld 494	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ∈ ℝ*)
6	4	simprd 495	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑦 ∈ ℝ*)
7	2	brel 5643	. . . . . . . . . 10 ⊢ (𝑦 ≤ 𝑧 → (𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*))
8	7	simprd 495	. . . . . . . . 9 ⊢ (𝑦 ≤ 𝑧 → 𝑧 ∈ ℝ*)
9	8	adantl 481	. . . . . . . 8 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑧 ∈ ℝ*)
10	5, 6, 9	3jca 1126	. . . . . . 7 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → (𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*))
11		xrletr 12821	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
12	10, 11	mpcom 38	. . . . . 6 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)
13	12	ax-gen 1799	. . . . 5 ⊢ ∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)
14	13	gen2 1800	. . . 4 ⊢ ∀𝑥∀𝑦∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)
15		cotr 6006	. . . 4 ⊢ (( ≤ ∘ ≤ ) ⊆ ≤ ↔ ∀𝑥∀𝑦∀𝑧((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))
16	14, 15	mpbir 230	. . 3 ⊢ ( ≤ ∘ ≤ ) ⊆ ≤
17		asymref 6010	. . . 4 ⊢ (( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) ↔ ∀𝑥 ∈ ∪ ∪ ≤ ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦))
18		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ* ∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))
19	2	brel 5643	. . . . . . . . . . . 12 ⊢ (𝑦 ≤ 𝑥 → (𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ*))
20	19	simpld 494	. . . . . . . . . . 11 ⊢ (𝑦 ≤ 𝑥 → 𝑦 ∈ ℝ*)
21	20	adantl 481	. . . . . . . . . 10 ⊢ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑦 ∈ ℝ*)
22		xrletri3 12817	. . . . . . . . . 10 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)))
23	21, 22	sylan2 592	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ* ∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)))
24	18, 23	mpbird 256	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ* ∧ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)) → 𝑥 = 𝑦)
25	24	ex 412	. . . . . . 7 ⊢ (𝑥 ∈ ℝ* → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))
26		xrleid 12814	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥)
27	26, 26	jca 511	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ* → (𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥))
28		breq2 5074	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑥 ↔ 𝑥 ≤ 𝑦))
29		breq1 5073	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑥 ↔ 𝑦 ≤ 𝑥))
30	28, 29	anbi12d 630	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥) ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)))
31	27, 30	syl5ibcom 244	. . . . . . 7 ⊢ (𝑥 ∈ ℝ* → (𝑥 = 𝑦 → (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥)))
32	25, 31	impbid 211	. . . . . 6 ⊢ (𝑥 ∈ ℝ* → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦))
33	32	alrimiv 1931	. . . . 5 ⊢ (𝑥 ∈ ℝ* → ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦))
34		lefld 18225	. . . . . 6 ⊢ ℝ* = ∪ ∪ ≤
35	34	eqcomi 2747	. . . . 5 ⊢ ∪ ∪ ≤ = ℝ*
36	33, 35	eleq2s 2857	. . . 4 ⊢ (𝑥 ∈ ∪ ∪ ≤ → ∀𝑦((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ 𝑥 = 𝑦))
37	17, 36	mprgbir 3078	. . 3 ⊢ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ )
38		xrex 12656	. . . . . 6 ⊢ ℝ* ∈ V
39	38, 38	xpex 7581	. . . . 5 ⊢ (ℝ* × ℝ*) ∈ V
40	39, 2	ssexi 5241	. . . 4 ⊢ ≤ ∈ V
41		isps 18201	. . . 4 ⊢ ( ≤ ∈ V → ( ≤ ∈ PosetRel ↔ (Rel ≤ ∧ ( ≤ ∘ ≤ ) ⊆ ≤ ∧ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ))))
42	40, 41	ax-mp 5	. . 3 ⊢ ( ≤ ∈ PosetRel ↔ (Rel ≤ ∧ ( ≤ ∘ ≤ ) ⊆ ≤ ∧ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ )))
43	1, 16, 37, 42	mpbir3an 1339	. 2 ⊢ ≤ ∈ PosetRel
44		xrletri 12816	. . . 4 ⊢ ((𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
45	44	rgen2 3126	. . 3 ⊢ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥)
46		qfto 6015	. . 3 ⊢ ((ℝ* × ℝ*) ⊆ ( ≤ ∪ ◡ ≤ ) ↔ ∀𝑥 ∈ ℝ* ∀𝑦 ∈ ℝ* (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
47	45, 46	mpbir 230	. 2 ⊢ (ℝ* × ℝ*) ⊆ ( ≤ ∪ ◡ ≤ )
48		ledm 18223	. . 3 ⊢ ℝ* = dom ≤
49	48	istsr 18216	. 2 ⊢ ( ≤ ∈ TosetRel ↔ ( ≤ ∈ PosetRel ∧ (ℝ* × ℝ*) ⊆ ( ≤ ∪ ◡ ≤ )))
50	43, 47, 49	mpbir2an 707	1 ⊢ ≤ ∈ TosetRel

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∧ w3a 1085  ∀wal 1537   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Vcvv 3422   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∪ cuni 4836   class class class wbr 5070   I cid 5479   × cxp 5578  ^◡ccnv 5579   ↾ cres 5582   ∘ ccom 5584  Rel wrel 5585  ℝ^*cxr 10939   ≤ cle 10941  PosetRelcps 18197   TosetRel ctsr 18198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-ps 18199  df-tsr 18200

This theorem is referenced by:  cnfldle  20519  cnfldfun  20522  cnfldfunALT  20523  letopon  22264  leordtval2  22271  leordtval  22272  iccordt  22273  ordtrestixx  22281  xrhaus  22444  xrge0tsms  23903  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  xrge0tsmsd  31219  cnvordtrestixx  31765  xrmulc1cn  31782  xrge0iifhmeo  31788  poimir  35737