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	⊢ ≤ ∈ TosetRel

Proof

Step	Hyp	Ref	Expression
1		lerel	⊢ Rel ≤
2		lerelxr	⊢ ≤ ⊆ ( ℝ* × ℝ* )
3	2	brel	⊢ ( 𝑥 ≤ 𝑦 → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
4	3	adantr	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
5	4	simpld	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ∈ ℝ* )
6	4	simprd	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑦 ∈ ℝ* )
7	2	brel	⊢ ( 𝑦 ≤ 𝑧 → ( 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
8	7	simprd	⊢ ( 𝑦 ≤ 𝑧 → 𝑧 ∈ ℝ* )
9	8	adantl	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑧 ∈ ℝ* )
10	5 6 9	3jca	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
11		xrletr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
12	10 11	mpcom	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 )
13	12	ax-gen	⊢ ∀ 𝑧 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 )
14	13	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 )
15		cotr	⊢ ( ( ≤ ∘ ≤ ) ⊆ ≤ ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
16	14 15	mpbir	⊢ ( ≤ ∘ ≤ ) ⊆ ≤
17		asymref	⊢ ( ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) ↔ ∀ 𝑥 ∈ ∪ ∪ ≤ ∀ 𝑦 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ 𝑥 = 𝑦 ) )
18		simpr	⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) )
19	2	brel	⊢ ( 𝑦 ≤ 𝑥 → ( 𝑦 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) )
20	19	simpld	⊢ ( 𝑦 ≤ 𝑥 → 𝑦 ∈ ℝ* )
21	20	adantl	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑦 ∈ ℝ* )
22		xrletri3	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
23	21 22	sylan2	⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
24	18 23	mpbird	⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) → 𝑥 = 𝑦 )
25	24	ex	⊢ ( 𝑥 ∈ ℝ* → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
26		xrleid	⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ 𝑥 )
27	26 26	jca	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥 ) )
28		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑥 ↔ 𝑥 ≤ 𝑦 ) )
29		breq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑥 ↔ 𝑦 ≤ 𝑥 ) )
30	28 29	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ≤ 𝑥 ∧ 𝑥 ≤ 𝑥 ) ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
31	27 30	syl5ibcom	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 = 𝑦 → ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ) )
32	25 31	impbid	⊢ ( 𝑥 ∈ ℝ* → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ 𝑥 = 𝑦 ) )
33	32	alrimiv	⊢ ( 𝑥 ∈ ℝ* → ∀ 𝑦 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ 𝑥 = 𝑦 ) )
34		lefld	⊢ ℝ* = ∪ ∪ ≤
35	34	eqcomi	⊢ ∪ ∪ ≤ = ℝ*
36	33 35	eleq2s	⊢ ( 𝑥 ∈ ∪ ∪ ≤ → ∀ 𝑦 ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ 𝑥 = 𝑦 ) )
37	17 36	mprgbir	⊢ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ )
38		xrex	⊢ ℝ* ∈ V
39	38 38	xpex	⊢ ( ℝ* × ℝ* ) ∈ V
40	39 2	ssexi	⊢ ≤ ∈ V
41		isps	⊢ ( ≤ ∈ V → ( ≤ ∈ PosetRel ↔ ( Rel ≤ ∧ ( ≤ ∘ ≤ ) ⊆ ≤ ∧ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) ) ) )
42	40 41	ax-mp	⊢ ( ≤ ∈ PosetRel ↔ ( Rel ≤ ∧ ( ≤ ∘ ≤ ) ⊆ ≤ ∧ ( ≤ ∩ ◡ ≤ ) = ( I ↾ ∪ ∪ ≤ ) ) )
43	1 16 37 42	mpbir3an	⊢ ≤ ∈ PosetRel
44		xrletri	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
45	44	rgen2	⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 )
46		qfto	⊢ ( ( ℝ* × ℝ* ) ⊆ ( ≤ ∪ ◡ ≤ ) ↔ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
47	45 46	mpbir	⊢ ( ℝ* × ℝ* ) ⊆ ( ≤ ∪ ◡ ≤ )
48		ledm	⊢ ℝ* = dom ≤
49	48	istsr	⊢ ( ≤ ∈ TosetRel ↔ ( ≤ ∈ PosetRel ∧ ( ℝ* × ℝ* ) ⊆ ( ≤ ∪ ◡ ≤ ) ) )
50	43 47 49	mpbir2an	⊢ ≤ ∈ TosetRel