# Metamath Proof Explorer

## Definition df-xrh

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

Ref Expression
Assertion df-xrh ${⊢}\mathrm{{ℝ}^{*}Hom}=\left({r}\in \mathrm{V}⟼\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cxrh ${class}\mathrm{{ℝ}^{*}Hom}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cxr ${class}{ℝ}^{*}$
5 3 cv ${setvar}{x}$
6 cr ${class}ℝ$
7 5 6 wcel ${wff}{x}\in ℝ$
8 crrh ${class}\mathrm{ℝHom}$
9 1 cv ${setvar}{r}$
10 9 8 cfv ${class}\mathrm{ℝHom}\left({r}\right)$
11 5 10 cfv ${class}\mathrm{ℝHom}\left({r}\right)\left({x}\right)$
12 cpnf ${class}\mathrm{+\infty }$
13 5 12 wceq ${wff}{x}=\mathrm{+\infty }$
14 club ${class}\mathrm{lub}$
15 9 14 cfv ${class}\mathrm{lub}\left({r}\right)$
16 10 6 cima ${class}\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]$
17 16 15 cfv ${class}\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)$
18 cglb ${class}\mathrm{glb}$
19 9 18 cfv ${class}\mathrm{glb}\left({r}\right)$
20 16 19 cfv ${class}\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)$
21 13 17 20 cif ${class}if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)$
22 7 11 21 cif ${class}if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)$
23 3 4 22 cmpt ${class}\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)$
24 1 2 23 cmpt ${class}\left({r}\in \mathrm{V}⟼\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)\right)$
25 0 24 wceq ${wff}\mathrm{{ℝ}^{*}Hom}=\left({r}\in \mathrm{V}⟼\left({x}\in {ℝ}^{*}⟼if\left({x}\in ℝ,\mathrm{ℝHom}\left({r}\right)\left({x}\right),if\left({x}=\mathrm{+\infty },\mathrm{lub}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right),\mathrm{glb}\left({r}\right)\left(\mathrm{ℝHom}\left({r}\right)\left[ℝ\right]\right)\right)\right)\right)\right)$