Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-xrh Structured version   Visualization version   GIF version

Definition df-xrh 29195
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
StepHypRef Expression
1 cxrh 29194 . 2 class *Hom
2 vr . . 3 setvar 𝑟
3 cvv 3172 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 cxr 9929 . . . 4 class *
64cv 1473 . . . . . 6 class 𝑥
7 cr 9791 . . . . . 6 class
86, 7wcel 1976 . . . . 5 wff 𝑥 ∈ ℝ
92cv 1473 . . . . . . 7 class 𝑟
10 crrh 29171 . . . . . . 7 class ℝHom
119, 10cfv 5790 . . . . . 6 class (ℝHom‘𝑟)
126, 11cfv 5790 . . . . 5 class ((ℝHom‘𝑟)‘𝑥)
13 cpnf 9927 . . . . . . 7 class +∞
146, 13wceq 1474 . . . . . 6 wff 𝑥 = +∞
1511, 7cima 5031 . . . . . . 7 class ((ℝHom‘𝑟) “ ℝ)
16 club 16711 . . . . . . . 8 class lub
179, 16cfv 5790 . . . . . . 7 class (lub‘𝑟)
1815, 17cfv 5790 . . . . . 6 class ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
19 cglb 16712 . . . . . . . 8 class glb
209, 19cfv 5790 . . . . . . 7 class (glb‘𝑟)
2115, 20cfv 5790 . . . . . 6 class ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
2214, 18, 21cif 4035 . . . . 5 class if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))
238, 12, 22cif 4035 . . . 4 class if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))
244, 5, 23cmpt 4637 . . 3 class (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))))
252, 3, 24cmpt 4637 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
261, 25wceq 1474 1 wff *Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
Colors of variables: wff setvar class
This definition is referenced by:  xrhval  29196
  Copyright terms: Public domain W3C validator