Theorem rrhval

Description: Value of the canonical homormorphism from the real numbers to a complete space. (Contributed by Thierry Arnoux, 2-Nov-2017)

	Ref	Expression
Hypotheses	rrhval.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
	rrhval.2	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
Assertion	rrhval	⊢ ( 𝑅 ∈ 𝑉 → ( ℝHom ‘ 𝑅 ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rrhval.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		rrhval.2	⊢ 𝐾 = ( TopOpen ‘ 𝑅 )
3		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
4	1	eqcomi	⊢ ( topGen ‘ ran (,) ) = 𝐽
5	4	a1i	⊢ ( 𝑟 = 𝑅 → ( topGen ‘ ran (,) ) = 𝐽 )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( TopOpen ‘ 𝑟 ) = ( TopOpen ‘ 𝑅 ) )
7	6 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( TopOpen ‘ 𝑟 ) = 𝐾 )
8	5 7	oveq12d	⊢ ( 𝑟 = 𝑅 → ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) = ( 𝐽 CnExt 𝐾 ) )
9		fveq2	⊢ ( 𝑟 = 𝑅 → ( ℚHom ‘ 𝑟 ) = ( ℚHom ‘ 𝑅 ) )
10	8 9	fveq12d	⊢ ( 𝑟 = 𝑅 → ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )
11		df-rrh	⊢ ℝHom = ( 𝑟 ∈ V ↦ ( ( ( topGen ‘ ran (,) ) CnExt ( TopOpen ‘ 𝑟 ) ) ‘ ( ℚHom ‘ 𝑟 ) ) )
12		fvex	⊢ ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) ∈ V
13	10 11 12	fvmpt	⊢ ( 𝑅 ∈ V → ( ℝHom ‘ 𝑅 ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )
14	3 13	syl	⊢ ( 𝑅 ∈ 𝑉 → ( ℝHom ‘ 𝑅 ) = ( ( 𝐽 CnExt 𝐾 ) ‘ ( ℚHom ‘ 𝑅 ) ) )