Theorem cnfldex 21239

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

Syntax hints:   ∈ wcel 2098  Vcvv 3468   ∪ cun 3941  {csn 4623  {ctp 4627  ⟨cop 4629   ∘ ccom 5673  ‘cfv 6536  (class class class)co 7404   ∈ cmpo 7406  ℂcc 11107   + caddc 11112   · cmul 11114   ≤ cle 11250   − cmin 11445  ∗ccj 15047  abscabs 15185  ndxcnx 17133  Basecbs 17151  +_gcplusg 17204  ._rcmulr 17205  *_𝑟cstv 17206  TopSetcts 17210  lecple 17211  distcds 17213  UnifSetcunif 17214  MetOpencmopn 21226  metUnifcmetu 21227  ℂ_fldccnfld 21236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-sn 4624  df-pr 4626  df-tp 4628  df-uni 4903  df-cnfld 21237

This theorem is referenced by:  regsumfsum  21325  rge0srg  21328  cnlmodlem3  25016  cnstrcvs  25019  cncvs  25023  cnncvsmulassdemo  25043  xrge0iifmhm  33449  xrge0pluscn  33450  xrge0tmd  33455  cnzh  33480  esumpfinvallem  33602  aacllem  48103