Theorem cnfldex 21316

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 5311. (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 21314	. 2 ⊢ ℂfld = (({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}))
2		tpex 7693	. . . 4 ⊢ {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∈ V
3		snex 5382	. . . 4 ⊢ {⟨(*𝑟‘ndx), ∗⟩} ∈ V
4	2, 3	unex 7691	. . 3 ⊢ ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))⟩, ⟨(.r‘ndx), (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))⟩} ∪ {⟨(*𝑟‘ndx), ∗⟩}) ∈ V
5		tpex 7693	. . . 4 ⊢ {⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∈ V
6		snex 5382	. . . 4 ⊢ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩} ∈ V
7	5, 6	unex 7691	. . 3 ⊢ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) ∈ V
8	4, 7	unex 7691	. 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 3441   ∪ cun 3900  {csn 4581  {ctp 4585  ⟨cop 4587   ∘ ccom 5629  ‘cfv 6493  (class class class)co 7360   ∈ cmpo 7362  ℂcc 11028   + caddc 11033   · cmul 11035   ≤ cle 11171   − cmin 11368  ∗ccj 15023  abscabs 15161  ndxcnx 17124  Basecbs 17140  +_gcplusg 17181  ._rcmulr 17182  *_𝑟cstv 17183  TopSetcts 17187  lecple 17188  distcds 17190  UnifSetcunif 17191  MetOpencmopn 21303  metUnifcmetu 21304  ℂ_fldccnfld 21313

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 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-sn 4582  df-pr 4584  df-tp 4586  df-uni 4865  df-cnfld 21314

This theorem is referenced by:  regsumfsum  21394  rge0srg  21397  cnlmodlem3  25098  cnstrcvs  25101  cncvs  25105  cnncvsmulassdemo  25124  gsumzrsum  33150  xrge0iifmhm  34098  xrge0pluscn  34099  xrge0tmd  34104  cnzh  34127  esumpfinvallem  34233  aacllem  50113