Definition df-rrh

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crrh	⊢ ℝHom
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		ctg	⊢ topGen
4		cioo	⊢ (,)
5	4	crn	⊢ ran (,)
6	5 3	cfv	⊢ ( topGen ‘ ran (,) )
7		ccnext	⊢ CnExt
8		ctopn	⊢ TopOpen
9	1	cv	⊢ 𝑟
10	9 8	cfv	⊢ ( TopOpen ‘ 𝑟 )
11	6 10 7	co	⊢ ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) )
12		cqqh	⊢ ℚHom
13	9 12	cfv	⊢ ( ℚHom ‘ 𝑟 )
14	13 11	cfv	⊢ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) )
15	1 2 14	cmpt	⊢ ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )
16	0 15	wceq	⊢ ℝHom = ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )