Theorem cnfldbas 17931

Description: The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.)

Assertion

Ref	Expression
cnfldbas	|- CC = ( Base ` ℂfld )

Proof of Theorem cnfldbas

Step	Hyp	Ref	Expression
1		cnex 9464	. 2 |- CC e. _V
2		cnfldstr 17929	. . 3 |- ℂfld Struct <. 1 , ; 1 3 >.
3		baseid 14322	. . 3 |- Base = Slot ( Base ` ndx )
4		snsstp1 4122	. . . 4 |- { <. ( Base ` ndx ) , CC >. } C_ { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
5		ssun1 3617	. . . . 5 |- { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } C_ ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
6		ssun1 3617	. . . . . 6 |- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
7		df-cnfld 17928	. . . . . 6 |- ℂfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. (TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , (metUnif ` ( abs o. - ) ) >. } ) )
8	6, 7	sseqtr4i 3487	. . . . 5 |- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) C_ ℂfld
9	5, 8	sstri 3463	. . . 4 |- { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } C_ ℂfld
10	4, 9	sstri 3463	. . 3 |- { <. ( Base ` ndx ) , CC >. } C_ ℂfld
11	2, 3, 10	strfv 14310	. 2 |- ( CC e. _V -> CC = ( Base ` ℂfld ) )
12	1, 11	ax-mp 5	1 |- CC = ( Base ` ℂfld )

Syntax hints:   = wceq 1370   e. wcel 1758   _Vcvv 3068   u. cun 3424   {csn 3975   {ctp 3979   <.cop 3981   o. ccom 4942   ` cfv 5516   CCcc 9381   1c1 9384   + caddc 9386   x. cmul 9388   <_ cle 9520   - cmin 9696   3c3 10473  ;cdc 10856   *ccj 12687   abscabs 12825   ndxcnx 14273   Basecbs 14276   +g cplusg 14340   .rcmulr 14341   *rcstv 14342  TopSetcts 14346   lecple 14347   distcds 14349   UnifSetcunif 14350   MetOpencmopn 17915  metUnifcmetu 17917  ℂ_fldccnfld 17927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-int 4227  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-1o 7020  df-oadd 7024  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-fin 7414  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-nn 10424  df-2 10481  df-3 10482  df-4 10483  df-5 10484  df-6 10485  df-7 10486  df-8 10487  df-9 10488  df-10 10489  df-n0 10681  df-z 10748  df-dec 10857  df-uz 10963  df-fz 11539  df-struct 14278  df-ndx 14279  df-slot 14280  df-base 14281  df-plusg 14353  df-mulr 14354  df-starv 14355  df-tset 14359  df-ple 14360  df-ds 14362  df-unif 14363  df-cnfld 17928

This theorem is referenced by:  cncrng  17946  cnfld0  17949  cnfld1  17950  cnfldneg  17951  cnfldplusf  17952  cnfldsub  17953  cndrng  17954  cnflddiv  17955  cnfldinv  17956  cnfldmulg  17957  cnfldexp  17958  cnsrng  17959  cnsubmlem  17970  cnsubglem  17971  cnsubrglem  17972  cnsubdrglem  17973  absabv  17979  cnsubrg  17982  cnmgpabl  17983  cnmsubglem  17984  gzrngunit  17987  gsumfsum  17988  expmhm  17989  nn0srg  17990  rge0srg  17991  zringbas  17998  zring0  18002  zrngbas  18004  zrng0  18008  dvdsrz  18011  zlpirlem1  18017  zlpirlem3  18019  zringunit  18023  zrngunit  18024  expghm  18032  expghmOLD  18033  cnmsgnbas  18117  psgninv  18121  zrhpsgnmhm  18123  rebase  18145  re0g  18151  regsumsupp  18161  cnfldms  20471  cnfldnm  20474  cnfldtopn  20477  cnfldtopon  20478  clmsscn  20767  cphsubrglem  20812  cphreccllem  20813  cphdivcl  20817  cphabscl  20820  cphsqrcl2  20821  cphsqrcl3  20822  cphipcl  20826  cncms  20983  cnflduss  20984  cnfldcusp  20985  resscdrg  20986  ishl2  20998  recms  21000  tdeglem3  21644  tdeglem4  21645  tdeglem2  21646  plypf1  21796  dvply2g  21867  dvply2  21868  dvnply  21870  taylfvallem  21939  taylf  21942  tayl0  21943  taylpfval  21946  taylply2  21949  taylply  21950  jensenlem1  22496  jensenlem2  22497  jensen  22498  amgmlem  22499  amgm  22500  wilthlem2  22523  wilthlem3  22524  dchrelbas2  22692  dchrelbas3  22693  dchrn0  22705  dchrghm  22711  dchrabs  22715  sum2dchr  22729  lgseisenlem4  22807  qrngbas  22984  cchhllem  23268  regsumfsum  26384  xrge0slmod  26446  iistmd  26466  xrge0iifmhm  26503  xrge0pluscn  26504  zringnm  26522  zzsnmOLD  26524  cnzh  26533  rezh  26534  cnrrext  26573  esumpfinvallem  26657  cnpwstotbnd  28834  repwsmet  28871  rrnequiv  28872  mzpmfpOLD  29222  cnsrexpcl  29660  fsumcnsrcl  29661  cnsrplycl  29662  rngunsnply  29668  proot1ex  29707  deg1mhm  29713