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 30189
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 30188 . 2 class *Hom
2 vr . . 3 setvar 𝑟
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 cxr 10111 . . . 4 class *
64cv 1522 . . . . . 6 class 𝑥
7 cr 9973 . . . . . 6 class
86, 7wcel 2030 . . . . 5 wff 𝑥 ∈ ℝ
92cv 1522 . . . . . . 7 class 𝑟
10 crrh 30165 . . . . . . 7 class ℝHom
119, 10cfv 5926 . . . . . 6 class (ℝHom‘𝑟)
126, 11cfv 5926 . . . . 5 class ((ℝHom‘𝑟)‘𝑥)
13 cpnf 10109 . . . . . . 7 class +∞
146, 13wceq 1523 . . . . . 6 wff 𝑥 = +∞
1511, 7cima 5146 . . . . . . 7 class ((ℝHom‘𝑟) “ ℝ)
16 club 16989 . . . . . . . 8 class lub
179, 16cfv 5926 . . . . . . 7 class (lub‘𝑟)
1815, 17cfv 5926 . . . . . 6 class ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
19 cglb 16990 . . . . . . . 8 class glb
209, 19cfv 5926 . . . . . . 7 class (glb‘𝑟)
2115, 20cfv 5926 . . . . . 6 class ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))
2214, 18, 21cif 4119 . . . . 5 class if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))
238, 12, 22cif 4119 . . . 4 class if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))
244, 5, 23cmpt 4762 . . 3 class (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ)))))
252, 3, 24cmpt 4762 . 2 class (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
261, 25wceq 1523 1 wff *Hom = (𝑟 ∈ V ↦ (𝑥 ∈ ℝ* ↦ if(𝑥 ∈ ℝ, ((ℝHom‘𝑟)‘𝑥), if(𝑥 = +∞, ((lub‘𝑟)‘((ℝHom‘𝑟) “ ℝ)), ((glb‘𝑟)‘((ℝHom‘𝑟) “ ℝ))))))
Colors of variables: wff setvar class
This definition is referenced by:  xrhval  30190
  Copyright terms: Public domain W3C validator