Metamath Proof Explorer


Theorem xrhval

Description: The value of the embedding from the extended real numbers into a complete lattice. (Contributed by Thierry Arnoux, 19-Feb-2018)

Ref Expression
Hypotheses xrhval.b B = ℝHom R
xrhval.l L = glb R
xrhval.u U = lub R
Assertion xrhval R V *Hom R = x * if x ℝHom R x if x = +∞ U B L B

Proof

Step Hyp Ref Expression
1 xrhval.b B = ℝHom R
2 xrhval.l L = glb R
3 xrhval.u U = lub R
4 elex R V R V
5 fveq2 r = R ℝHom r = ℝHom R
6 5 fveq1d r = R ℝHom r x = ℝHom R x
7 fveq2 r = R lub r = lub R
8 7 3 syl6eqr r = R lub r = U
9 5 imaeq1d r = R ℝHom r = ℝHom R
10 9 1 syl6eqr r = R ℝHom r = B
11 8 10 fveq12d r = R lub r ℝHom r = U B
12 fveq2 r = R glb r = glb R
13 12 2 syl6eqr r = R glb r = L
14 13 10 fveq12d r = R glb r ℝHom r = L B
15 11 14 ifeq12d r = R if x = +∞ lub r ℝHom r glb r ℝHom r = if x = +∞ U B L B
16 6 15 ifeq12d r = R if x ℝHom r x if x = +∞ lub r ℝHom r glb r ℝHom r = if x ℝHom R x if x = +∞ U B L B
17 16 mpteq2dv r = R x * if x ℝHom r x if x = +∞ lub r ℝHom r glb r ℝHom r = x * if x ℝHom R x if x = +∞ U B L B
18 df-xrh *Hom = r V x * if x ℝHom r x if x = +∞ lub r ℝHom r glb r ℝHom r
19 xrex * V
20 19 mptex x * if x ℝHom R x if x = +∞ U B L B V
21 17 18 20 fvmpt R V *Hom R = x * if x ℝHom R x if x = +∞ U B L B
22 4 21 syl R V *Hom R = x * if x ℝHom R x if x = +∞ U B L B