Definition df-xrh 34631

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 34630	. 2 class ℝ*Hom
2		vr	. . 3 setvar 𝑟
3		cvv 3451	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5		cxr 11323	. . . 4 class ℝ*
6	4	cv 1569	. . . . . 6 class 𝑥
7		cr 11180	. . . . . 6 class ℝ
8	6, 7	wcel 2145	. . . . 5 wff 𝑥 ∈ ℝ
9	2	cv 1569	. . . . . . 7 class 𝑟
10		crrh 34607	. . . . . . 7 class ℝHom
11	9, 10	cfv 6531	. . . . . 6 class (ℝHom‘𝑟)
12	6, 11	cfv 6531	. . . . 5 class ((ℝHom‘𝑟)‘𝑥)
13		cpnf 11321	. . . . . . 7 class +∞
14	6, 13	wceq 1570	. . . . . 6 wff 𝑥 = +∞
15	11, 7	cima 5654	. . . . . . 7 class ((ℝHom‘𝑟) “ ℝ)
16		club 18463	. . . . . . . 8 class lub
17	9, 16	cfv 6531	. . . . . . 7 class (lub‘𝑟)
18	15, 17	cfv 6531	. . . . . 6 class ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
19		cglb 18464	. . . . . . . 8 class glb
20	9, 19	cfv 6531	. . . . . . 7 class (glb‘𝑟)
21	15, 20	cfv 6531	. . . . . 6 class ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
22	14, 18, 21	cif 4482	. . . . 5 class if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))
23	8, 12, 22	cif 4482	. . . 4 class if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))
24	4, 5, 23	cmpt 5186	. . 3 class (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))))
25	2, 3, 24	cmpt 5186	. 2 class (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
26	1, 25	wceq 1570	1 wff ℝ*Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))

This definition is used by:  xrhval  34632