Definition df-rrh 30039

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	|- RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) ) ` (QQHom ` r ) ) )

Detailed syntax breakdown of Definition df-rrh

Step	Hyp	Ref	Expression
1		crrh 30037	. 2 class RRHom
2		vr	. . 3 setvar r
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class r
5		cqqh 30016	. . . . 5 class QQHom
6	4, 5	cfv 5888	. . . 4 class (QQHom ` r )
7		cioo 12175	. . . . . . 7 class (,)
8	7	crn 5115	. . . . . 6 class ran (,)
9		ctg 16098	. . . . . 6 class topGen
10	8, 9	cfv 5888	. . . . 5 class ( topGen ` ran (,) )
11		ctopn 16082	. . . . . 6 class TopOpen
12	4, 11	cfv 5888	. . . . 5 class ( TopOpen ` r )
13		ccnext 21863	. . . . 5 class CnExt
14	10, 12, 13	co 6650	. . . 4 class ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) )
15	6, 14	cfv 5888	. . 3 class ( ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) ) ` (QQHom ` r ) )
16	2, 3, 15	cmpt 4729	. 2 class ( r e. _V |-> ( ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) ) ` (QQHom ` r ) ) )
17	1, 16	wceq 1483	1 wff RRHom = ( r e. _V |-> ( ( ( topGen ` ran (,) )CnExt ( TopOpen ` r ) ) ` (QQHom ` r ) ) )

This definition is referenced by:  rrhval  30040