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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxrh
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cxr	$$class{ℝ}^{*}$$
5	3	cv	$$setvarx$$
6		cr	$$classℝ$$
7	5 6	wcel	$$wffx\in ℝ$$
8		crrh	$$class\mathrm{ℝHom}$$
9	1	cv	$$setvarr$$
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	$$wffx=\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	$$classif\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	$$classif\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