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	⊢ ℝ*Hom = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxrh	⊢ ℝ*Hom
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cxr	⊢ ℝ*
5	3	cv	⊢ 𝑥
6		cr	⊢ ℝ
7	5 6	wcel	⊢ 𝑥 ∈ ℝ
8		crrh	⊢ ℝHom
9	1	cv	⊢ 𝑟
10	9 8	cfv	⊢ ( ℝHom ‘ 𝑟 )
11	5 10	cfv	⊢ ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 )
12		cpnf	⊢ +∞
13	5 12	wceq	⊢ 𝑥 = +∞
14		club	⊢ lub
15	9 14	cfv	⊢ ( lub ‘ 𝑟 )
16	10 6	cima	⊢ ( ( ℝHom ‘ 𝑟 ) “ ℝ )
17	16 15	cfv	⊢ ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) )
18		cglb	⊢ glb
19	9 18	cfv	⊢ ( glb ‘ 𝑟 )
20	16 19	cfv	⊢ ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) )
21	13 17 20	cif	⊢ if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) )
22	7 11 21	cif	⊢ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) )
23	3 4 22	cmpt	⊢ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) )
24	1 2 23	cmpt	⊢ ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) ) )
25	0 24	wceq	⊢ ℝ*Hom = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 ∈ ℝ , ( ( ℝHom ‘ 𝑟 ) ‘ 𝑥 ) , if ( 𝑥 = +∞ , ( ( lub ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) , ( ( glb ‘ 𝑟 ) ‘ ( ( ℝHom ‘ 𝑟 ) “ ℝ ) ) ) ) ) )