Theorem fvexi 6907

Description: The value of a class exists. Inference form of fvex 6906. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fvexi.1	⊢ 𝐴 = (𝐹‘𝐵)

Assertion

Ref	Expression
fvexi	⊢ 𝐴 ∈ V

Proof of Theorem fvexi

Step	Hyp	Ref	Expression
1		fvexi.1	. 2 ⊢ 𝐴 = (𝐹‘𝐵)
2		fvex 6906	. 2 ⊢ (𝐹‘𝐵) ∈ V
3	1, 2	eqeltri 2822	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1534   ∈ wcel 2099  Vcvv 3462  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5303

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-sn 4624  df-pr 4626  df-uni 4906  df-iota 6498  df-fv 6554

This theorem is referenced by:  mptfvmpt  7237  ovex  7449  mapfienlem1  9441  climle  15637  climsup  15669  iserabs  15814  isumshft  15838  explecnv  15864  prodfclim1  15892  ressbas  17243  ressbasOLD  17244  ressbas2  17246  ressid  17253  ressval3d  17255  ressval3dOLD  17256  topnid  17445  prdsplusg  17468  prdsmulr  17469  prdsvsca  17470  prdsip  17471  prdsle  17472  prdsds  17474  prdshom  17477  prdsco  17478  pwselbasb  17498  pwsvscafval  17504  pwssca  17506  pwssnf1o  17508  imassca  17529  imasvsca  17530  imasle  17533  xpsrnbas  17581  xpssca  17586  xpsvsca  17587  isacs2  17661  homffval  17698  comfffval  17706  oppchomfval  17722  oppchomfvalOLD  17723  oppccofval  17725  oppccatid  17729  monfval  17743  oppcmon  17749  sectffval  17761  invffval  17769  rescbas  17840  rescbasOLD  17841  reschom  17842  rescco  17844  resccoOLD  17845  fullsubc  17864  isfunc  17878  isfuncd  17879  idfu2nd  17891  idfu1st  17893  cofu1st  17897  cofu2nd  17899  fucco  17982  fucid  17991  invfuc  17994  initoval  18010  termoval  18011  homafval  18046  arwval  18060  coafval  18081  coapm  18088  setccatid  18101  catchomfval  18119  catccofval  18121  catccatid  18123  elestrchom  18146  estrccatid  18150  xpcbas  18197  xpchomfval  18198  xpccofval  18201  1stf1  18211  1stf2  18212  2ndf1  18214  2ndf2  18215  prf1  18219  prf2fval  18220  evlf2  18238  evlf1  18240  curf1fval  18244  curf11  18246  curf12  18247  curf1cl  18248  curf2  18249  curf2cl  18251  hof2fval  18275  yonedalem4a  18295  yonedalem4c  18297  yonedalem3  18300  yonedainv  18301  isdrs  18321  ispos  18334  odupos  18348  pltfval  18351  lubfval  18370  lubeldm  18373  lubval  18376  glbfval  18383  glbeldm  18386  glbval  18389  odulub  18427  odujoin  18428  oduglb  18429  odumeet  18430  clatlem  18522  clatlubcl2  18524  clatglbcl2  18526  isdlat  18542  ipolt  18555  ipopos  18556  isacs4lem  18564  plusffval  18634  issstrmgm  18641  gsumvalx  18664  gsumval  18665  ismgmhm  18684  issubmgm2  18691  submgmacs  18705  issubmnd  18749  ress0g  18750  ismhm  18770  mndvcl  18782  0subm  18802  0mhm  18804  submacs  18812  pwsdiagmhm  18816  gsumz  18821  frmdplusg  18839  efmndplusg  18865  efmndmgm  18870  smndex1mgm  18892  grpinvfval  18968  grpsubfval  18973  grpsubfvalALT  18974  mulgfval  19059  mulgfvalALT  19060  mulgval  19061  issubg  19116  0subg  19141  0subgOLD  19142  subgacs  19151  nsgacs  19152  nmznsg  19158  eqgfval  19166  isghm  19205  isghmOLD  19206  gicen  19268  isga  19281  subgga  19290  orbstafun  19301  orbstaval  19302  orbsta  19303  cntzfval  19310  cntzval  19311  oppgplusfval  19338  symg2bas  19386  symgvalstruct  19390  symgvalstructOLD  19391  cayleylem2  19407  psgnfval  19494  odfval  19526  odinf  19557  dfod2  19558  0subgALT  19562  pgpfi1  19589  pgp0  19590  sylow1lem2  19593  sylow3lem6  19626  lsmfval  19632  lsmvalx  19633  oppglsm  19636  pj1fval  19688  efglem  19710  efgrelexlemb  19744  efgcpbllemb  19749  frgpeccl  19755  frgpmhm  19759  vrgpval  19761  frgpuplem  19766  frgpupf  19767  frgpupval  19768  frgpup1  19769  frgpup3lem  19771  frgpnabllem2  19868  iscygodd  19882  prmcyg  19888  lt6abl  19889  gsumval3a  19897  gsumval3  19901  gsumzres  19903  gsumzcl2  19904  gsumzf1o  19906  gsumreidx  19911  gsumzaddlem  19915  gsumzadd  19916  gsumzsplit  19921  gsummptshft  19930  gsumzmhm  19931  gsumzoppg  19938  gsumzinv  19939  gsummptfidminv  19941  gsumsub  19942  gsumpt  19956  gsummptf1o  19957  gsum2dlem1  19964  gsum2dlem2  19965  gsum2d  19966  gsum2d2lem  19967  gsumxp2  19974  fsfnn0gsumfsffz  19977  nn0gsumfz  19978  gsummptnn0fz  19980  dprdfid  20013  dprdfinv  20015  dprdfadd  20016  dprdfeq0  20018  dmdprdsplitlem  20033  dpjidcl  20054  ablfacrplem  20061  ablfacrp  20062  ablfacrp2  20063  ablfac1a  20065  ablfac1b  20066  ablfac1c  20067  ablfac1eu  20069  pgpfaclem2  20078  ablfaclem2  20082  ablfaclem3  20083  2nsgsimpgd  20098  prmgrpsimpgd  20110  ablsimpgprmd  20111  mgpplusg  20117  mgpress  20128  mgpressOLD  20129  issrg  20167  ring1ne0  20274  gsumdixp  20294  pwsmgp  20302  opprmulfval  20314  dvdsrval  20339  isunit  20351  unitgrp  20361  unitlinv  20371  unitrinv  20372  dvrfval  20380  rdivmuldivd  20391  rnghmval  20418  isrnghm  20419  c0snmgmhm  20440  c0snmhm  20441  isnzr2  20496  isnzr2hash  20497  0ring  20504  0ringdif  20505  01eq0ringOLD  20509  0ring01eqbi  20510  zrrnghm  20514  issubrg  20551  subrgugrp  20571  rngcrescrhm  20658  rrgval  20671  rrgsupp  20675  isdrng2  20717  drngmclOLD  20725  drngid2  20726  imadrhmcl  20772  subrgacs  20775  sdrgacs  20776  cntzsdrg  20777  subdrgint  20778  isabv  20786  staffval  20816  islmod  20836  scaffval  20852  lcomfsupp  20874  mptscmfsupp0  20899  rmodislmod  20902  rmodislmodOLD  20903  lssset  20906  islss  20907  lsssn0  20921  lssacs  20940  lspfval  20946  lspval  20948  lspcl  20949  lspuni0  20983  lss0v  20990  0lmhm  21014  lmhmvsca  21019  islbs  21050  islbs3  21132  lbsextlem1  21135  lbsextlem3  21137  lbsextlem4  21138  lbsext  21140  rnglidl0  21214  rsp1  21222  2idlval  21236  qusrhm  21261  expghm  21461  zrhrhmb  21496  zlmvsca  21511  zntoslem  21550  znfi  21553  znunithash  21558  psgnghm  21572  psgnghm2  21573  psgnevpmb  21579  ipffval  21640  ocvfval  21658  ocvval  21659  elocv  21660  thlbas  21688  thlbasOLD  21689  thlle  21690  thlleOLD  21691  thlleval  21692  thloc  21693  pjfval  21700  pjdm  21701  pjpm  21702  isobs  21714  frlmbas  21749  frlmbasf  21754  frlmvscafval  21760  frlmvscavalb  21764  frlmsslss2  21769  frlmip  21772  uvcvval  21780  uvcvvcl  21781  frlmssuvc2  21789  frlmsslsp  21790  ellspd  21796  elfilspd  21797  islinds2  21807  islindf4  21832  aspval  21866  psrbas  21938  psrelbas  21939  psrplusg  21941  psrmulr  21947  psrvscafval  21953  psrvscacl  21956  psr0lid  21958  psrlidm  21967  psrridm  21968  resspsradd  21980  resspsrmul  21981  resspsrvsca  21982  psrascl  21984  mvrval2  21988  mplsubglem  22004  mpllsslem  22005  mplsubrglem  22009  ressmpladd  22032  ressmplmul  22033  ressmplvsca  22034  mplmon  22038  mplmonmul  22039  mplcoe1  22040  opsrle  22050  opsrtoslem2  22065  mplmon2  22070  evlslem4  22085  psrbagev1  22086  psrbagev1OLD  22087  evlslem2  22090  evlslem3  22091  evlsval2  22098  selvval  22126  mhpval  22130  ismhp3  22133  psdfval  22148  coe1sfi  22199  coe1fsupp  22200  mptcoe1fsupp  22201  coe1ae0  22202  ressply1add  22215  ressply1mul  22216  ressply1vsca  22217  gsumply1subr  22219  psropprmul  22223  coe1tmmul2fv  22265  coe1pwmulfv  22267  ply1coe  22286  cply1coe0  22289  cply1coe0bi  22290  gsummoncoe1  22296  evls1fval  22307  evls1val  22308  evls1rhmlem  22309  evls1sca  22311  evls1gsumadd  22312  evls1gsummul  22313  evl1val  22317  evl1fval1lem  22318  fveval1fvcl  22321  evl1sca  22322  evl1var  22324  evl1addd  22329  evl1subd  22330  evl1muld  22331  evl1expd  22333  pf1f  22338  pf1mpf  22340  pf1ind  22343  evl1gsummul  22348  evls1expd  22355  evls1fpws  22357  evls1addd  22359  evls1muld  22360  evls1vsca  22361  rhmply1vr1  22375  mamures  22385  mamucl  22389  mamuvs1  22393  mamuvs2  22394  matbas2d  22413  matecl  22415  mamumat1cl  22429  mat1comp  22430  mamulid  22431  mamurid  22432  mat1ov  22438  matsc  22440  mat1dimelbas  22461  mat1dimmul  22466  mat1f1o  22468  dmatval  22482  dmatmulcl  22490  scmatval  22494  scmatscmiddistr  22498  mavmulcl  22537  1mavmul  22538  marrepfval  22550  marrepeval  22553  marepvfval  22555  submafval  22569  mdetfval  22576  mdetunilem9  22610  mdetuni0  22611  m2detleiblem3  22619  m2detleiblem4  22620  minmar1fval  22636  minmar1eval  22639  symgmatr01  22644  gsummatr01lem3  22647  gsummatr01  22649  smadiadetlem1a  22653  smadiadetlem3  22658  invrvald  22666  cpmat  22699  mat2pmatfval  22713  mat2pmatbas  22716  decpmatfsupp  22759  decpmatmulsumfsupp  22763  pmatcollpw3lem  22773  pmatcollpw3fi1lem2  22777  pm2mpval  22785  mply1topmatcl  22795  chmatval  22819  chpmatfval  22820  chfacffsupp  22846  chfacfscmul0  22848  chfacfscmulfsupp  22849  chfacfpmmul0  22852  chfacfpmmulfsupp  22853  cpmidpmatlem2  22861  cpmadumatpolylem1  22871  imastopn  23712  uzrest  23889  tmdgsum2  24088  distgp  24091  indistgp  24092  snclseqg  24108  tsmsval  24123  tsms0  24134  tsmsres  24136  tsmsxplem1  24145  tsmsxplem2  24146  ussid  24253  isusp  24254  ressust  24256  cnextucn  24296  prdsxmetlem  24362  nrmmetd  24571  nmfval  24585  tngds  24652  tngdsOLD  24653  tngnm  24656  tngngp2  24657  tngngpd  24658  tngngp  24659  tngngp3  24661  nmo0  24740  xrrest  24811  climcncf  24908  cphsubrglem  25193  cphcjcl  25199  tcphex  25233  ipcau2  25250  cmsss  25367  rrxip  25406  minveclem4a  25446  minveclem4  25448  mbflimsup  25683  mbflim  25685  mdegfval  26086  mdegleb  26088  mdegldg  26090  deg1val  26120  uc1pval  26164  mon1pval  26166  q1pval  26179  r1pval  26182  ply1remlem  26189  ply1rem  26190  fta1glem1  26192  fta1glem2  26193  fta1blem  26195  idomrootle  26197  ig1pval  26200  elqaalem3  26346  ulmcau  26421  ulmdvlem1  26426  ulmdvlem3  26428  mbfulm  26432  itgulm  26434  dchrplusg  27273  dchrmullid  27278  dchrinvcl  27279  dchrptlem2  27291  dchrptlem3  27292  dchrsum2  27294  sumdchr2  27296  dchr2sum  27299  axtgcont1  28392  tgjustc1  28399  tgjustc2  28400  tglowdim1  28424  tgldimor  28426  tgldim0eq  28427  iscgrgd  28437  isismt  28458  tglnfn  28471  tglnunirn  28472  tglngval  28475  legval  28508  ishlg  28526  hlcgrex  28540  hlcgreulem  28541  mirval  28579  midexlem  28616  israg  28621  perpln1  28634  perpln2  28635  isperp  28636  ishpg  28683  midf  28700  ismidb  28702  lmif  28709  islmib  28711  iscgra  28733  isinag  28762  isleag  28771  iseqlg  28791  ttgval  28799  ttgvalOLD  28800  ttgitvval  28812  setsvtx  28968  uhgrunop  29008  incistruhgr  29012  upgrunop  29052  umgrunop  29054  usgriedgleord  29161  uspgredgleord  29165  uhgr0vsize0  29172  lfuhgr1v0e  29187  uhgrspanop  29229  upgrspanop  29230  umgrspanop  29231  usgrspanop  29232  uhgrspan1lem1  29233  upgrres1lem1  29242  usgredgffibi  29257  fusgredgfi  29258  usgr1v0e  29259  nbgr2vtx1edg  29283  nbuhgr2vtx1edgb  29285  nbfusgrlevtxm1  29310  nbfusgrlevtxm2  29311  uvtx01vtx  29330  cplgr1vlem  29362  cplgr1v  29363  cusgrsize2inds  29387  cusgrfilem3  29391  sizusglecusg  29397  fusgrmaxsize  29398  vtxdgfval  29401  vtxdun  29415  vtxd0nedgb  29422  p1evtxdeqlem  29446  p1evtxdeq  29447  p1evtxdp1  29448  usgrvd0nedg  29467  vtxdginducedm1lem1  29473  vtxdginducedm1lem4  29476  vtxdginducedm1  29477  vtxdginducedm1fi  29478  finsumvtxdg2ssteplem4  29482  rusgrnumwrdl2  29520  wksfval  29543  iswlkg  29547  wlkonprop  29592  wlkp1lem3  29609  wlkp1lem8  29614  wlkp1  29615  wksonproplem  29638  wksonproplemOLD  29639  wwlks  29766  wwlksnon  29782  wspthsnon  29783  clwwlk  29913  0wlkonlem2  30049  conngrv2edg  30125  eupthp1  30146  eupth2eucrct  30147  eupthvdres  30165  eupth2lem3  30166  eupth2lemb  30167  3cyclfrgrrn  30216  frgrwopreglem1  30242  frgrwopreg1  30248  imsmetlem  30620  dipfval  30632  sspval  30653  islno  30683  nmooval  30693  nmounbseqi  30707  nmobndseqi  30709  0ofval  30717  0oval  30718  ajfval  30739  isph  30752  phpar  30754  ajval  30791  ubthlem1  30800  ubthlem2  30801  minvecolem4b  30808  minvecolem4  30810  minvecolem5  30811  hlex  30828  ressplusf  32830  ressnm  32831  oppglt  32835  ressprs  32836  oduprs  32837  ismnt  32856  mgcval  32860  gsummptres  32924  gsummptres2  32925  gsumpart  32927  gsumhashmul  32929  inftmrel  33049  isinftm  33050  gsumvsca1  33094  ress1r  33104  ringinvval  33105  dvrcan5  33106  rmfsupp2  33108  erlval  33118  rlocval  33119  rlocbas  33127  rlocaddval  33128  rlocmulval  33129  rlocf1  33133  fldgenval  33167  ofldlt1  33196  resvsca  33209  quslmod  33239  islinds5  33248  ellspds  33249  elrsp  33253  linds2eq  33262  elringlsm  33274  lsmsnpridl  33279  grplsm0l  33284  qusima  33289  nsgmgc  33293  nsgqusf1o  33297  elrspunidl  33309  elrspunsn  33310  drngidlhash  33315  prmidl0  33331  oppreqg  33364  opprqusbas  33369  qsdrngi  33376  idlsrgbas  33385  idlsrgplusg  33386  idlsrgmulr  33388  idlsrgtset  33389  rprmval  33397  1arithidom  33418  fply1  33437  evls1fvf  33441  evl1fvf  33442  coe1zfv  33465  r1pquslmic  33484  resssra  33490  dimval  33501  dimvalfi  33502  lvecdim0  33507  ply1degltdimlem  33523  irngval  33567  elirng  33568  irngss  33569  irngnzply1lem  33572  minplyval  33580  constrsuc  33610  constrelextdg2  33619  mdetpmtr1  33651  rspectopn  33695  zarcls0  33696  zarcls  33702  zartopn  33703  zarmxt1  33708  rhmpreimacnlem  33712  rhmpreimacn  33713  pstmfval  33724  ordtrest2NEW  33751  ordtconnlem1  33752  fsumcvg4  33778  pl1cn  33783  qqhval  33802  sibf0  34181  sitgclg  34189  sitgaddlemb  34195  eulerpartlemgvv  34223  afsval  34530  pthhashvtx  34968  usgrcyclgt2v  34972  cusgr3cyclex  34977  acycgr2v  34991  cusgracyclt3v  34997  mrsubfval  35349  mrsubcv  35351  mrsubff  35353  mrsubrn  35354  elmrsubrn  35361  msubfval  35365  msubff  35371  mpstval  35376  elmpst  35377  msrval  35379  mstaval  35385  msubvrs  35401  mclsssvlem  35403  mclsval  35404  mclsind  35411  mppsval  35413  climlec3  35569  sdclem2  37456  sdclem1  37457  caures  37474  heiborlem3  37527  heibor  37535  grpokerinj  37607  rngoi  37613  dvrunz  37668  isdrngo1  37670  isdrngo2  37672  isrngohom  37679  idlval  37727  isidl  37728  0idl  37739  0rngo  37741  divrngidl  37742  smprngopr  37766  igenval  37775  lshpset  38689  lsatset  38701  lcvfbr  38731  islfl  38771  lfl0f  38780  lfl1  38781  lfladd0l  38785  lflnegl  38787  lflvscl  38788  lflvsdi1  38789  lflvsdi2  38790  lflvsdi2a  38791  lflvsass  38792  lfl0sc  38793  lflsc0N  38794  lfl1sc  38795  lkr0f  38805  lkrsc  38808  eqlkr2  38811  ldualvbase  38837  ldualfvadd  38839  ldualvaddval  38842  ldualsca  38843  ldualfvs  38847  ldualvsval  38849  isopos  38891  cmtfvalN  38921  cvrfval  38979  pats  38996  glbconNOLD  39089  llnset  39217  lplnset  39241  lvolset  39284  lineset  39450  isline  39451  pointsetN  39453  psubspset  39456  ispsubsp  39457  pmapval  39469  paddfval  39509  paddval  39510  pclfvalN  39601  pclvalN  39602  polfvalN  39616  polvalN  39617  psubclsetN  39648  ispsubclN  39649  watvalN  39705  lhpset  39707  lautset  39794  islaut  39795  pautsetN  39810  ispautN  39811  ldilset  39821  ltrnset  39830  dilsetN  39865  cdleme26e  40071  cdleme26eALTN  40073  cdleme26fALTN  40074  cdleme26f  40075  cdleme26f2ALTN  40076  cdleme26f2  40077  cdlemefs32sn1aw  40126  cdleme43fsv1snlem  40132  cdleme41sn3a  40145  cdleme32a  40153  cdleme40m  40179  cdleme40n  40180  cdleme42b  40190  tgrpbase  40458  tgrpopr  40459  istendo  40472  tendopl  40488  tendo02  40499  erngbase  40513  erngfplus  40514  erngfmul  40517  erngbase-rN  40521  erngfplus-rN  40522  erngfmul-rN  40525  cdlemk36  40625  cdlemkid  40648  dvasca  40718  dvavbase  40725  dvafvadd  40726  dvafvsca  40728  diafval  40743  diaval  40744  dvhsca  40794  dvhvbase  40799  dvhfvadd  40803  dvhfvsca  40812  docafvalN  40834  docavalN  40835  djafvalN  40846  djavalN  40847  dibfval  40853  dibopelvalN  40855  dibopelval2  40857  dibelval3  40859  diblsmopel  40883  dicfval  40887  dicval  40888  cdlemn11a  40919  dihvalcqpre  40947  dihopelvalcpre  40960  dihord6apre  40968  dihpN  41048  dochfval  41062  dochval  41063  djhfval  41109  djhval  41110  islpolN  41195  lpolconN  41199  dochpolN  41202  lcfrlem9  41262  lcd0vvalN  41325  mapdval  41340  mapd1o  41360  mapdunirnN  41362  mapdhval  41436  mapdhval0  41437  hvmapfval  41471  hvmapval  41472  hdmap1fval  41508  hdmap1vallem  41509  hgmapfval  41598  hlhilset  41646  hlhilbase  41648  hlhilplus  41649  hlhilvsca  41663  hlhilip  41664  hlhilnvl  41666  hlhillsm  41672  hlhillcs  41674  hashscontpow  41834  frlmfielbas  42190  fimgmcyc  42224  frlm0vald  42229  evlsval3  42249  evlsbagval  42256  selvcllem5  42272  evlselv  42277  fsuppind  42280  fsuppssind  42283  mhpind  42284  mhphf  42287  sn-isghm  42365  islssfgi  42770  pwssplit4  42787  frlmpwfi  42796  mendplusgfval  42883  mendmulrfval  42885  mendvscafval  42888  idomodle  42893  deg1mhm  42902  mnringelbased  43925  mnring0g2d  43931  mnringmulrd  43932  mnringmulrcld  43939  dvgrat  44023  uzmptshftfval  44057  climexp  45262  climinf  45263  climneg  45267  climdivf  45269  climconstmpt  45315  climresmpt  45316  climsubmpt  45317  fnlimfvre  45331  limsupvaluz  45365  limsupequzmpt2  45375  climuzlem  45400  climisp  45403  climxrrelem  45406  climxrre  45407  limsupgtlem  45434  liminflelimsupuz  45442  liminfgelimsupuz  45445  liminfequzmpt2  45448  liminfvaluz  45449  limsupvaluz3  45455  climliminflimsupd  45458  liminfreuzlem  45459  liminfltlem  45461  liminflimsupclim  45464  liminflbuz2  45472  liminfpnfuz  45473  xlimclim2lem  45496  climxlim2  45503  sge0isum  46084  sge0uzfsumgt  46101  sge0seq  46103  meaiunlelem  46125  caragendifcl  46171  omeiunle  46174  omeiunltfirp  46176  carageniuncl  46180  caragensal  46182  opnssborel  46292  smflimlem6  46433  smfpimcc  46465  smflimmpt  46467  smflimsuplem4  46480  smflimsuplem6  46482  smflimsuplem8  46484  smfliminflem  46487  clnbgrlevtx  47448  isisubgr  47465  isubgriedg  47466  isubgrvtx  47468  uspgrimprop  47488  isuspgrim  47490  gricen  47509  ushggricedg  47511  uhgrimisgrgric  47514  grlicen  47543  upwlksfval  47548  isupwlkg  47550  copisnmnd  47582  zlidlring  47647  cznrng  47674  cznnring  47675  rngchomfvalALTV  47680  rngccofvalALTV  47683  rngccatidALTV  47685  rngcrescrhmALTV  47693  ringchomfvalALTV  47714  ringccofvalALTV  47717  ringccatidALTV  47719  ofaddmndmap  47758  suppmptcfin  47794  mptcfsupp  47795  dmatALTbas  47820  lcoop  47830  linccl  47833  lcosn0  47839  lincvalsc0  47840  lcoc0  47841  linc0scn0  47842  linc1  47844  lincscmcl  47851  islinindfis  47868  lincext1  47873  lincext2  47874  lindslinindimp2lem2  47878  lindslinindimp2lem3  47879  lindsrng01  47887  snlindsntorlem  47889  snlindsntor  47890  ldepspr  47892  lincresunit1  47896  lincresunit2  47897  lines  48155  line  48156  rrxlines  48157  sphere  48171  rrxsphere  48172  functhinclem1  48398  thincciso  48406