Theorem cnfldex 21329

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 5314. (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 21327	. 2 ⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
2		tpex 7703	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∈ V
3		snex 5387	. . . 4 ⊢ {⟨(*𝑟‘ndx), ∗⟩} ∈ V
4	2, 3	unex 7701	. . 3 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∈ V
5		tpex 7703	. . . 4 ⊢ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∈ V
6		snex 5387	. . . 4 ⊢ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩} ∈ V
7	5, 6	unex 7701	. . 3 ⊢ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) ∈ V
8	4, 7	unex 7701	. 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 2833	1 ⊢ ℂfld ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901  {csn 4582  {ctp 4586  ⟨cop 4588   ∘ ccom 5638  ‘cfv 6502  (class class class)co 7370   ∈ cmpo 7372  ℂcc 11038   + caddc 11043   · cmul 11045   ≤ cle 11181   − cmin 11378  ∗ccj 15033  abscabs 15171  ndxcnx 17134  Basecbs 17150  +_gcplusg 17191  ._rcmulr 17192  *_𝑟cstv 17193  TopSetcts 17197  lecple 17198  distcds 17200  UnifSetcunif 17201  MetOpencmopn 21316  metUnifcmetu 21317  ℂ_fldccnfld 21326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-tp 4587  df-uni 4866  df-cnfld 21327

This theorem is referenced by:  regsumfsum  21407  rge0srg  21410  cnlmodlem3  25111  cnstrcvs  25114  cncvs  25118  cnncvsmulassdemo  25137  gsumzrsum  33165  xrge0iifmhm  34123  xrge0pluscn  34124  xrge0tmd  34129  cnzh  34152  esumpfinvallem  34258  aacllem  50189