Theorem cnfldex 21294

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 5301. (Revised by GG, 16-Mar-2025.)

Assertion

Ref	Expression
cnfldex	⊢ ℂfld ∈ V

Proof of Theorem cnfldex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cnfld 21292	. 2 ⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
2		tpex 7679	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∈ V
3		snex 5372	. . . 4 ⊢ {⟨(*𝑟‘ndx), ∗⟩} ∈ V
4	2, 3	unex 7677	. . 3 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∈ V
5		tpex 7679	. . . 4 ⊢ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∈ V
6		snex 5372	. . . 4 ⊢ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩} ∈ V
7	5, 6	unex 7677	. . 3 ⊢ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) ∈ V
8	4, 7	unex 7677	. 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 2827	1 ⊢ ℂfld ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∪ cun 3895  {csn 4573  {ctp 4577  ⟨cop 4579   ∘ ccom 5618  ‘cfv 6481  (class class class)co 7346   ∈ cmpo 7348  ℂcc 11004   + caddc 11009   · cmul 11011   ≤ cle 11147   − cmin 11344  ∗ccj 15003  abscabs 15141  ndxcnx 17104  Basecbs 17120  +_gcplusg 17161  ._rcmulr 17162  *_𝑟cstv 17163  TopSetcts 17167  lecple 17168  distcds 17170  UnifSetcunif 17171  MetOpencmopn 21281  metUnifcmetu 21282  ℂ_fldccnfld 21291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-sn 4574  df-pr 4576  df-tp 4578  df-uni 4857  df-cnfld 21292

This theorem is referenced by:  regsumfsum  21372  rge0srg  21375  cnlmodlem3  25065  cnstrcvs  25068  cncvs  25072  cnncvsmulassdemo  25091  gsumzrsum  33039  xrge0iifmhm  33952  xrge0pluscn  33953  xrge0tmd  33958  cnzh  33981  esumpfinvallem  34087  aacllem  49912