Definition df-xrh 34273

Description: Define an embedding from the extended real number into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018.)

Assertion

Ref	Expression
df-xrh	⊢ ℝ*Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))

Distinct variable group:   𝑥,𝑟

Detailed syntax breakdown of Definition df-xrh

Step	Hyp	Ref	Expression
1		cxrh 34272	. 2 class ℝ*Hom
2		vr	. . 3 setvar 𝑟
3		cvv 3453	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		cxr 11210	. . . 4 class ℝ*
6	4	cv 1558	. . . . . 6 class 𝑥
7		cr 11067	. . . . . 6 class ℝ
8	6, 7	wcel 2141	. . . . 5 wff 𝑥 ∈ ℝ
9	2	cv 1558	. . . . . . 7 class 𝑟
10		crrh 34249	. . . . . . 7 class ℝHom
11	9, 10	cfv 6515	. . . . . 6 class (ℝHom‘𝑟)
12	6, 11	cfv 6515	. . . . 5 class ((ℝHom‘𝑟)‘𝑥)
13		cpnf 11208	. . . . . . 7 class +∞
14	6, 13	wceq 1559	. . . . . 6 wff 𝑥 = +∞
15	11, 7	cima 5648	. . . . . . 7 class ((ℝHom‘𝑟) “ ℝ)
16		club 18322	. . . . . . . 8 class lub
17	9, 16	cfv 6515	. . . . . . 7 class (lub‘𝑟)
18	15, 17	cfv 6515	. . . . . 6 class ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
19		cglb 18323	. . . . . . . 8 class glb
20	9, 19	cfv 6515	. . . . . . 7 class (glb‘𝑟)
21	15, 20	cfv 6515	. . . . . 6 class ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
22	14, 18, 21	cif 4479	. . . . 5 class if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))
23	8, 12, 22	cif 4479	. . . 4 class if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))
24	4, 5, 23	cmpt 5180	. . 3 class (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))))
25	2, 3, 24	cmpt 5180	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
26	1, 25	wceq 1559	1 wff ℝ*Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))

This definition is referenced by:  xrhval  34274