Metamath Proof Explorer

Theorem cnfldtset

Description: The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 31-Mar-2025) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026)

Ref Expression
Assertion cnfldtset ⊢ MetOpen ⁡ abs ∘ − = TopSet ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 fvex ⊢ MetOpen ⁡ abs ∘ − ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 21
3 tsetid ⊢ TopSet = Slot TopSet ⁡ ndx
4 snsstp1 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ −
5 ssun1 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs
6 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs ⊆ Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs
7 df-cnfld ⊢ ℂ fld = Base ndx ℂ + ndx u ∈ ℂ , v ∈ ℂ ⟼ u + v ⋅ ndx u ∈ ℂ , v ∈ ℂ ⟼ u ⁢ v ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs
8 6 7 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − EuclF ⁡ ndx abs ⊆ ℂ fld
9 5 8 sstri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ⊆ ℂ fld
10 4 9 sstri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ⊆ ℂ fld
11 2 3 10 strfv ⊢ MetOpen ⁡ abs ∘ − ∈ V → MetOpen ⁡ abs ∘ − = TopSet ⁡ ℂ fld
12 1 11 ax-mp ⊢ MetOpen ⁡ abs ∘ − = TopSet ⁡ ℂ fld