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=\mathrm{ℝHom}\left(R\right)\left[ℝ\right]$$
	xrhval.l	$$⊢L=\mathrm{glb}\left(R\right)$$
	xrhval.u	$$⊢U=\mathrm{lub}\left(R\right)$$
Assertion	xrhval

Proof

Step	Hyp	Ref	Expression
1		xrhval.b	$$⊢B=\mathrm{ℝHom}\left(R\right)\left[ℝ\right]$$
2		xrhval.l	$$⊢L=\mathrm{glb}\left(R\right)$$
3		xrhval.u	$$⊢U=\mathrm{lub}\left(R\right)$$
4		elex	$$⊢R\in V\to R\in \mathrm{V}$$
5		fveq2	$$⊢r=R\to \mathrm{ℝHom}\left(r\right)=\mathrm{ℝHom}\left(R\right)$$
6	5	fveq1d	$$⊢r=R\to \mathrm{ℝHom}\left(r\right)\left(x\right)=\mathrm{ℝHom}\left(R\right)\left(x\right)$$
7		fveq2	$$⊢r=R\to \mathrm{lub}\left(r\right)=\mathrm{lub}\left(R\right)$$
8	7 3	eqtr4di	$$⊢r=R\to \mathrm{lub}\left(r\right)=U$$
9	5	imaeq1d	$$⊢r=R\to \mathrm{ℝHom}\left(r\right)\left[ℝ\right]=\mathrm{ℝHom}\left(R\right)\left[ℝ\right]$$
10	9 1	eqtr4di	$$⊢r=R\to \mathrm{ℝHom}\left(r\right)\left[ℝ\right]=B$$
11	8 10	fveq12d	$$⊢r=R\to \mathrm{lub}\left(r\right)\left(\mathrm{ℝHom}\left(r\right)\left[ℝ\right]\right)=U\left(B\right)$$
12		fveq2	$$⊢r=R\to \mathrm{glb}\left(r\right)=\mathrm{glb}\left(R\right)$$
13	12 2	eqtr4di	$$⊢r=R\to \mathrm{glb}\left(r\right)=L$$
14	13 10	fveq12d	$$⊢r=R\to \mathrm{glb}\left(r\right)\left(\mathrm{ℝHom}\left(r\right)\left[ℝ\right]\right)=L\left(B\right)$$
15	11 14	ifeq12d	$$⊢r=R\to 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)=if\left(x=\mathrm{+\infty },U\left(B\right),L\left(B\right)\right)$$
16	6 15	ifeq12d	$$⊢r=R\to 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)=if\left(x\in ℝ,\mathrm{ℝHom}\left(R\right)\left(x\right),if\left(x=\mathrm{+\infty },U\left(B\right),L\left(B\right)\right)\right)$$
17	16	mpteq2dv	$$⊢r=R\to \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)=\left(x\in {ℝ}^{*}⟼if\left(x\in ℝ,\mathrm{ℝHom}\left(R\right)\left(x\right),if\left(x=\mathrm{+\infty },U\left(B\right),L\left(B\right)\right)\right)\right)$$
18		df-xrh
19		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
20	19	mptex	$$⊢\left(x\in {ℝ}^{*}⟼if\left(x\in ℝ,\mathrm{ℝHom}\left(R\right)\left(x\right),if\left(x=\mathrm{+\infty },U\left(B\right),L\left(B\right)\right)\right)\right)\in \mathrm{V}$$
21	17 18 20	fvmpt
22	4 21	syl