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)

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

Proof

Step Hyp Ref Expression
1 fvex ⊢ MetOpen ⁡ abs ∘ − ∈ V
2 cnfldstr ⊢ ℂ fld Struct 1 13
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 ∘ −
6 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ 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 ∘ −
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 ∘ −
8 6 7 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ 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