Theorem recms

Description: The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017)

	Ref	Expression
Assertion	recms	|- RRfld e. CMetSp

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2	1	recld2	|- RR e. ( Clsd ` ( TopOpen ` CCfld ) )
3		cncms	|- CCfld e. CMetSp
4		ax-resscn	|- RR C_ CC
5		df-refld	|- RRfld = ( CCfld |`s RR )
6		cnfldbas	|- CC = ( Base ` CCfld )
7	5 6 1	cmsss	|- ( ( CCfld e. CMetSp /\ RR C_ CC ) -> ( RRfld e. CMetSp <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) ) )
8	3 4 7	mp2an	|- ( RRfld e. CMetSp <-> RR e. ( Clsd ` ( TopOpen ` CCfld ) ) )
9	2 8	mpbir	|- RRfld e. CMetSp