Definition df-rrh 31945

Description: Define the canonical homomorphism from the real numbers to any complete field, as the extension by continuity of the canonical homomorphism from the rational numbers. (Contributed by Mario Carneiro, 22-Oct-2017.) (Revised by Thierry Arnoux, 23-Oct-2017.)

Assertion

Ref	Expression
df-rrh	⊢ ℝHom = (𝑟 ∈ V ↦ (((topGen‘ran (,))CnExt(TopOpen‘𝑟))‘(ℚHom‘𝑟)))

Detailed syntax breakdown of Definition df-rrh

Step	Hyp	Ref	Expression
1		crrh 31943	. 2 class ℝHom
2		vr	. . 3 setvar 𝑟
3		cvv 3432	. . 3 class V
4	2	cv 1538	. . . . 5 class 𝑟
5		cqqh 31922	. . . . 5 class ℚHom
6	4, 5	cfv 6433	. . . 4 class (ℚHom‘𝑟)
7		cioo 13079	. . . . . . 7 class (,)
8	7	crn 5590	. . . . . 6 class ran (,)
9		ctg 17148	. . . . . 6 class topGen
10	8, 9	cfv 6433	. . . . 5 class (topGen‘ran (,))
11		ctopn 17132	. . . . . 6 class TopOpen
12	4, 11	cfv 6433	. . . . 5 class (TopOpen‘𝑟)
13		ccnext 23210	. . . . 5 class CnExt
14	10, 12, 13	co 7275	. . . 4 class ((topGen‘ran (,))CnExt(TopOpen‘𝑟))
15	6, 14	cfv 6433	. . 3 class (((topGen‘ran (,))CnExt(TopOpen‘𝑟))‘(ℚHom‘𝑟))
16	2, 3, 15	cmpt 5157	. 2 class (𝑟 ∈ V ↦ (((topGen‘ran (,))CnExt(TopOpen‘𝑟))‘(ℚHom‘𝑟)))
17	1, 16	wceq 1539	1 wff ℝHom = (𝑟 ∈ V ↦ (((topGen‘ran (,))CnExt(TopOpen‘𝑟))‘(ℚHom‘𝑟)))

This definition is referenced by:  rrhval  31946