Metamath Proof Explorer

Theorem resscdrg

Description: The real numbers are a subset of any complete subfield in the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis resscdrg.1 ⊢F=ℂfld↾𝑠K
Assertion resscdrg ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→ℝ⊆K

Proof

Step Hyp Ref Expression
1 resscdrg.1 ⊢F=ℂfld↾𝑠K
2 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
3 2 cnfldtop ⊢TopOpen⁡ℂfld∈Top
4 ax-resscn ⊢ℝ⊆ℂ
5 qssre ⊢ℚ⊆ℝ
6 unicntop ⊢ℂ=⋃TopOpen⁡ℂfld
7 2 tgioo2 ⊢topGen⁡ran⁡.=TopOpen⁡ℂfld↾𝑡ℝ
8 6 7 restcls ⊢TopOpen⁡ℂfld∈Top∧ℝ⊆ℂ∧ℚ⊆ℝ→cls⁡topGen⁡ran⁡.⁡ℚ=cls⁡TopOpen⁡ℂfld⁡ℚ∩ℝ
9 3 4 5 8 mp3an ⊢cls⁡topGen⁡ran⁡.⁡ℚ=cls⁡TopOpen⁡ℂfld⁡ℚ∩ℝ
10 qdensere ⊢cls⁡topGen⁡ran⁡.⁡ℚ=ℝ
11 9 10 eqtr3i ⊢cls⁡TopOpen⁡ℂfld⁡ℚ∩ℝ=ℝ
12 sseqin2 ⊢ℝ⊆cls⁡TopOpen⁡ℂfld⁡ℚ↔cls⁡TopOpen⁡ℂfld⁡ℚ∩ℝ=ℝ
13 11 12 mpbir ⊢ℝ⊆cls⁡TopOpen⁡ℂfld⁡ℚ
14 simp3 ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→F∈CMetSp
15 cncms ⊢ℂfld∈CMetSp
16 cnfldbas ⊢ℂ=Baseℂfld
17 16 subrgss ⊢K∈SubRing⁡ℂfld→K⊆ℂ
18 17 3ad2ant1 ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→K⊆ℂ
19 1 16 2 cmsss ⊢ℂfld∈CMetSp∧K⊆ℂ→F∈CMetSp↔K∈Clsd⁡TopOpen⁡ℂfld
20 15 18 19 sylancr ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→F∈CMetSp↔K∈Clsd⁡TopOpen⁡ℂfld
21 14 20 mpbid ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→K∈Clsd⁡TopOpen⁡ℂfld
22 1 eleq1i ⊢F∈DivRing↔ℂfld↾𝑠K∈DivRing
23 qsssubdrg ⊢K∈SubRing⁡ℂfld∧ℂfld↾𝑠K∈DivRing→ℚ⊆K
24 22 23 sylan2b ⊢K∈SubRing⁡ℂfld∧F∈DivRing→ℚ⊆K
25 24 3adant3 ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→ℚ⊆K
26 6 clsss2 ⊢K∈Clsd⁡TopOpen⁡ℂfld∧ℚ⊆K→cls⁡TopOpen⁡ℂfld⁡ℚ⊆K
27 21 25 26 syl2anc ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→cls⁡TopOpen⁡ℂfld⁡ℚ⊆K
28 13 27 sstrid ⊢K∈SubRing⁡ℂfld∧F∈DivRing∧F∈CMetSp→ℝ⊆K