Metamath Proof Explorer

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 = r ∈ V ⟼ x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxrh class ℝ *Hom
1 vr setvar r
2 cvv class V
3 vx setvar x
4 cxr class ℝ *
5 3 cv setvar x
6 cr class ℝ
7 5 6 wcel wff x ∈ ℝ
8 crrh class ℝHom
9 1 cv setvar r
10 9 8 cfv class ℝHom ⁡ r
11 5 10 cfv class ℝHom ⁡ r ⁡ x
12 cpnf class +∞
13 5 12 wceq wff x = +∞
14 club class lub
15 9 14 cfv class lub ⁡ r
16 10 6 cima class ℝHom ⁡ r ℝ
17 16 15 cfv class lub ⁡ r ⁡ ℝHom ⁡ r ℝ
18 cglb class glb
19 9 18 cfv class glb ⁡ r
20 16 19 cfv class glb ⁡ r ⁡ ℝHom ⁡ r ℝ
21 13 17 20 cif class if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ
22 7 11 21 cif class if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ
23 3 4 22 cmpt class x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ
24 1 2 23 cmpt class r ∈ V ⟼ x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ
25 0 24 wceq wff ℝ *Hom = r ∈ V ⟼ x ∈ ℝ * ⟼ if x ∈ ℝ ℝHom ⁡ r ⁡ x if x = +∞ lub ⁡ r ⁡ ℝHom ⁡ r ℝ glb ⁡ r ⁡ ℝHom ⁡ r ℝ