Theorem cnfldex 21287

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

Syntax hints:   ∈ wcel 2098  Vcvv 3471   ∪ cun 3945  {csn 4630  {ctp 4634  ⟨cop 4636   ∘ ccom 5684  ‘cfv 6551  (class class class)co 7424   ∈ cmpo 7426  ℂcc 11142   + caddc 11147   · cmul 11149   ≤ cle 11285   − cmin 11480  ∗ccj 15081  abscabs 15219  ndxcnx 17167  Basecbs 17185  +_gcplusg 17238  ._rcmulr 17239  *_𝑟cstv 17240  TopSetcts 17244  lecple 17245  distcds 17247  UnifSetcunif 17248  MetOpencmopn 21274  metUnifcmetu 21275  ℂ_fldccnfld 21284

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 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431  ax-un 7744

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-sn 4631  df-pr 4633  df-tp 4635  df-uni 4911  df-cnfld 21285

This theorem is referenced by:  regsumfsum  21373  rge0srg  21376  cnlmodlem3  25083  cnstrcvs  25086  cncvs  25090  cnncvsmulassdemo  25110  xrge0iifmhm  33545  xrge0pluscn  33546  xrge0tmd  33551  cnzh  33576  esumpfinvallem  33698  aacllem  48285