# Metamath Proof Explorer

## Theorem cnfldfunALT

Description: Alternate proof of cnfldfun (much shorter proof, using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld ). (Contributed by AV, 18-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT $⊢ Fun ⁡ ℂ fld$

### Proof

Step Hyp Ref Expression
1 cnfldstr $⊢ ℂ fld Struct 1 13$
2 structn0fun $⊢ ℂ fld Struct 1 13 → Fun ⁡ ℂ fld ∖ ∅$
3 fvex $⊢ Base ndx ∈ V$
4 cnex $⊢ ℂ ∈ V$
5 3 4 opnzi $⊢ Base ndx ℂ ≠ ∅$
6 5 nesymi $⊢ ¬ ∅ = Base ndx ℂ$
7 fvex $⊢ + ndx ∈ V$
8 addex $⊢ + ∈ V$
9 7 8 opnzi $⊢ + ndx + ≠ ∅$
10 9 nesymi $⊢ ¬ ∅ = + ndx +$
11 fvex $⊢ ⋅ ndx ∈ V$
12 mulex $⊢ × ∈ V$
13 11 12 opnzi $⊢ ⋅ ndx × ≠ ∅$
14 13 nesymi $⊢ ¬ ∅ = ⋅ ndx ×$
15 3ioran $⊢ ¬ ∅ = Base ndx ℂ ∨ ∅ = + ndx + ∨ ∅ = ⋅ ndx × ↔ ¬ ∅ = Base ndx ℂ ∧ ¬ ∅ = + ndx + ∧ ¬ ∅ = ⋅ ndx ×$
16 0ex $⊢ ∅ ∈ V$
17 16 eltp $⊢ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ↔ ∅ = Base ndx ℂ ∨ ∅ = + ndx + ∨ ∅ = ⋅ ndx ×$
18 15 17 xchnxbir $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ↔ ¬ ∅ = Base ndx ℂ ∧ ¬ ∅ = + ndx + ∧ ¬ ∅ = ⋅ ndx ×$
19 6 10 14 18 mpbir3an $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx ×$
20 fvex $⊢ * ndx ∈ V$
21 cjf $⊢ * : ℂ ⟶ ℂ$
22 fex $⊢ * : ℂ ⟶ ℂ ∧ ℂ ∈ V → * ∈ V$
23 21 4 22 mp2an $⊢ * ∈ V$
24 20 23 opnzi $⊢ * ndx * ≠ ∅$
25 24 necomi $⊢ ∅ ≠ * ndx *$
26 nelsn $⊢ ∅ ≠ * ndx * → ¬ ∅ ∈ * ndx *$
27 25 26 ax-mp $⊢ ¬ ∅ ∈ * ndx *$
28 19 27 pm3.2i $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∧ ¬ ∅ ∈ * ndx *$
29 fvex $⊢ TopSet ⁡ ndx ∈ V$
30 fvex $⊢ MetOpen ⁡ abs ∘ − ∈ V$
31 29 30 opnzi $⊢ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≠ ∅$
32 31 nesymi $⊢ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ −$
33 fvex $⊢ ≤ ndx ∈ V$
34 letsr $⊢ ≤ ∈ TosetRel$
35 34 elexi $⊢ ≤ ∈ V$
36 33 35 opnzi $⊢ ≤ ndx ≤ ≠ ∅$
37 36 nesymi $⊢ ¬ ∅ = ≤ ndx ≤$
38 fvex $⊢ dist ⁡ ndx ∈ V$
39 absf $⊢ abs : ℂ ⟶ ℝ$
40 fex $⊢ abs : ℂ ⟶ ℝ ∧ ℂ ∈ V → abs ∈ V$
41 39 4 40 mp2an $⊢ abs ∈ V$
42 subf $⊢ − : ℂ × ℂ ⟶ ℂ$
43 4 4 xpex $⊢ ℂ × ℂ ∈ V$
44 fex $⊢ − : ℂ × ℂ ⟶ ℂ ∧ ℂ × ℂ ∈ V → − ∈ V$
45 42 43 44 mp2an $⊢ − ∈ V$
46 41 45 coex $⊢ abs ∘ − ∈ V$
47 38 46 opnzi $⊢ dist ⁡ ndx abs ∘ − ≠ ∅$
48 47 nesymi $⊢ ¬ ∅ = dist ⁡ ndx abs ∘ −$
49 3ioran $⊢ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∨ ∅ = ≤ ndx ≤ ∨ ∅ = dist ⁡ ndx abs ∘ − ↔ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∧ ¬ ∅ = ≤ ndx ≤ ∧ ¬ ∅ = dist ⁡ ndx abs ∘ −$
50 32 37 48 49 mpbir3an $⊢ ¬ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∨ ∅ = ≤ ndx ≤ ∨ ∅ = dist ⁡ ndx abs ∘ −$
51 16 eltp $⊢ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ↔ ∅ = TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ∨ ∅ = ≤ ndx ≤ ∨ ∅ = dist ⁡ ndx abs ∘ −$
52 50 51 mtbir $⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ −$
53 fvex $⊢ UnifSet ⁡ ndx ∈ V$
54 fvex $⊢ metUnif ⁡ abs ∘ − ∈ V$
55 53 54 opnzi $⊢ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ≠ ∅$
56 55 necomi $⊢ ∅ ≠ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
57 nelsn $⊢ ∅ ≠ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − → ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
58 56 57 ax-mp $⊢ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
59 52 58 pm3.2i $⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∧ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
60 28 59 pm3.2i $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∧ ¬ ∅ ∈ * ndx * ∧ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∧ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
61 ioran $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ∨ ∅ ∈ 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 ∘ −$
62 ioran $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ↔ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∧ ¬ ∅ ∈ * ndx *$
63 ioran $⊢ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ↔ ¬ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∧ ¬ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
64 62 63 anbi12i $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ∧ ¬ ∅ ∈ 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 ∘ −$
65 61 64 bitri $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ∨ ∅ ∈ 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 ∘ −$
66 60 65 mpbir $⊢ ¬ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ∨ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
67 df-cnfld $⊢ ℂ fld = Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
68 67 eleq2i $⊢ ∅ ∈ ℂ fld ↔ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
69 elun $⊢ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∪ 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 ∘ −$
70 elun $⊢ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ↔ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx *$
71 elun $⊢ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∪ UnifSet ⁡ ndx metUnif ⁡ abs ∘ − ↔ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
72 70 71 orbi12i $⊢ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∪ * ndx * ∨ ∅ ∈ 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 ∘ −$
73 68 69 72 3bitri $⊢ ∅ ∈ ℂ fld ↔ ∅ ∈ Base ndx ℂ + ndx + ⋅ ndx × ∨ ∅ ∈ * ndx * ∨ ∅ ∈ TopSet ⁡ ndx MetOpen ⁡ abs ∘ − ≤ ndx ≤ dist ⁡ ndx abs ∘ − ∨ ∅ ∈ UnifSet ⁡ ndx metUnif ⁡ abs ∘ −$
74 66 73 mtbir $⊢ ¬ ∅ ∈ ℂ fld$
75 disjsn $⊢ ℂ fld ∩ ∅ = ∅ ↔ ¬ ∅ ∈ ℂ fld$
76 74 75 mpbir $⊢ ℂ fld ∩ ∅ = ∅$
77 disjdif2 $⊢ ℂ fld ∩ ∅ = ∅ → ℂ fld ∖ ∅ = ℂ fld$
78 76 77 ax-mp $⊢ ℂ fld ∖ ∅ = ℂ fld$
79 78 funeqi $⊢ Fun ⁡ ℂ fld ∖ ∅ ↔ Fun ⁡ ℂ fld$
80 2 79 sylib $⊢ ℂ fld Struct 1 13 → Fun ⁡ ℂ fld$
81 1 80 ax-mp $⊢ Fun ⁡ ℂ fld$