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

Metamath Proof Explorer

Theorem cnfldcjOLD

Description: Obsolete version of cnfldcj as of 27-Apr-2025. (Contributed by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Revised by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldcjOLD ⊢ * = * ℂ fld

Proof

Step Hyp Ref Expression
1 cjf ⊢ * : ℂ ⟶ ℂ
2 cnex ⊢ ℂ ∈ V
3 fex2 ⊢ * : ℂ ⟶ ℂ ∧ ℂ ∈ V ∧ ℂ ∈ V → * ∈ V
4 1 2 2 3 mp3an ⊢ * ∈ V
5 cnfldstrOLD ⊢ ℂ fld Struct 1 13
6 starvid ⊢ ∗ 𝑟 = Slot * ndx
7 ssun2 ⊢ * ndx * ⊆ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx *
8 ssun1 ⊢ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ⊆ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
9 dfcnfldOLD ⊢ ℂ fld = Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −
10 8 9 sseqtrri ⊢ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ⊆ ℂ fld
11 7 10 sstri ⊢ * ndx * ⊆ ℂ fld
12 5 6 11 strfv ⊢ * ∈ V → * = * ℂ fld
13 4 12 ax-mp ⊢ * = * ℂ fld