![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnfldex | Structured version Visualization version GIF version |
Description: The field of complex numbers is a set. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Avoid complex number axioms and ax-pow 5369. (Revised by GG, 16-Mar-2025.) |
Ref | Expression |
---|---|
cnfldex | ⊢ ℂfld ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-cnfld 21344 | . 2 ⊢ ℂfld = (({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∪ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉})) | |
2 | tpex 7755 | . . . 4 ⊢ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∈ V | |
3 | snex 5437 | . . . 4 ⊢ {〈(*𝑟‘ndx), ∗〉} ∈ V | |
4 | 2, 3 | unex 7754 | . . 3 ⊢ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∈ V |
5 | tpex 7755 | . . . 4 ⊢ {〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∈ V | |
6 | snex 5437 | . . . 4 ⊢ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉} ∈ V | |
7 | 5, 6 | unex 7754 | . . 3 ⊢ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉}) ∈ V |
8 | 4, 7 | unex 7754 | . 2 ⊢ (({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))〉, 〈(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∪ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉})) ∈ V |
9 | 1, 8 | eqeltri 2822 | 1 ⊢ ℂfld ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Vcvv 3462 ∪ cun 3945 {csn 4633 {ctp 4637 〈cop 4639 ∘ ccom 5686 ‘cfv 6554 (class class class)co 7424 ∈ cmpo 7426 ℂcc 11156 + caddc 11161 · cmul 11163 ≤ cle 11299 − cmin 11494 ∗ccj 15101 abscabs 15239 ndxcnx 17195 Basecbs 17213 +gcplusg 17266 .rcmulr 17267 *𝑟cstv 17268 TopSetcts 17272 lecple 17273 distcds 17275 UnifSetcunif 17276 MetOpencmopn 21333 metUnifcmetu 21334 ℂfldccnfld 21343 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-sn 4634 df-pr 4636 df-tp 4638 df-uni 4914 df-cnfld 21344 |
This theorem is referenced by: regsumfsum 21432 rge0srg 21435 cnlmodlem3 25156 cnstrcvs 25159 cncvs 25163 cnncvsmulassdemo 25183 xrge0iifmhm 33754 xrge0pluscn 33755 xrge0tmd 33760 cnzh 33785 esumpfinvallem 33907 aacllem 48549 |
Copyright terms: Public domain | W3C validator |