Definition df-xrh 30061

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	|- RR*Hom = ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) ) ) )

Distinct variable group:   x, r

Detailed syntax breakdown of Definition df-xrh

Step	Hyp	Ref	Expression
1		cxrh 30060	. 2 class RR*Hom
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5		cxr 10073	. . . 4 class RR*
6	4	cv 1482	. . . . . 6 class x
7		cr 9935	. . . . . 6 class RR
8	6, 7	wcel 1990	. . . . 5 wff x e. RR
9	2	cv 1482	. . . . . . 7 class r
10		crrh 30037	. . . . . . 7 class RRHom
11	9, 10	cfv 5888	. . . . . 6 class (RRHom ` r )
12	6, 11	cfv 5888	. . . . 5 class ( (RRHom ` r ) ` x )
13		cpnf 10071	. . . . . . 7 class +oo
14	6, 13	wceq 1483	. . . . . 6 wff x = +oo
15	11, 7	cima 5117	. . . . . . 7 class ( (RRHom ` r ) " RR )
16		club 16942	. . . . . . . 8 class lub
17	9, 16	cfv 5888	. . . . . . 7 class ( lub ` r )
18	15, 17	cfv 5888	. . . . . 6 class ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) )
19		cglb 16943	. . . . . . . 8 class glb
20	9, 19	cfv 5888	. . . . . . 7 class ( glb ` r )
21	15, 20	cfv 5888	. . . . . 6 class ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) )
22	14, 18, 21	cif 4086	. . . . 5 class if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) )
23	8, 12, 22	cif 4086	. . . 4 class if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) )
24	4, 5, 23	cmpt 4729	. . 3 class ( x e. RR* |-> if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) ) )
25	2, 3, 24	cmpt 4729	. 2 class ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) ) ) )
26	1, 25	wceq 1483	1 wff RR*Hom = ( r e. _V |-> ( x e. RR* |-> if ( x e. RR , ( (RRHom ` r ) ` x ) , if ( x = +oo , ( ( lub ` r ) ` ( (RRHom ` r ) " RR ) ) , ( ( glb ` r ) ` ( (RRHom ` r ) " RR ) ) ) ) ) )

This definition is referenced by:  xrhval  30062