This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldunifOLD

Description: Obsolete version of cnfldunif as of 27-Apr-2025. (Contributed by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldunifOLD ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 fvex ⊢ metUnif ⁡ abs ∘ − ∈ V
2 cnfldstrOLD ⊢ ℂ fld Struct 1 13
3 unifid ⊢ UnifSet = Slot UnifSet ⁡ ndx
4 ssun2 ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
5 ssun2 ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
6 dfcnfldOLD ⊢ ℂ fld = Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
7 5 6 sseqtrri ⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
8 4 7 sstri ⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ⊆ ℂ fld
9 2 3 8 strfv ⊢ metUnif ⁡ abs ∘ − ∈ V → metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld
10 1 9 ax-mp ⊢ metUnif ⁡ abs ∘ − = UnifSet ⁡ ℂ fld