Theorem plusgslid 13131

Description: Slot property of +_g. (Contributed by Jim Kingdon, 3-Feb-2023.)

Assertion

Ref	Expression
plusgslid	⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)

Proof of Theorem plusgslid

Step	Hyp	Ref	Expression
1		df-plusg 13109	. 2 ⊢ +g = Slot 2
2		2nn 9260	. 2 ⊢ 2 ∈ ℕ
3	1, 2	ndxslid 13043	1 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)

Syntax hints:   ∧ wa 104   = wceq 1395   ∈ wcel 2200  ‘cfv 5314  ℕcn 9098  2c2 9149  ndxcnx 13015  Slot cslot 13017  +_gcplusg 13096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4521  ax-cnex 8078  ax-resscn 8079  ax-1re 8081  ax-addrcl 8084

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-int 3923  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4381  df-xp 4722  df-rel 4723  df-cnv 4724  df-co 4725  df-dm 4726  df-rn 4727  df-res 4728  df-iota 5274  df-fun 5316  df-fv 5322  df-ov 5997  df-inn 9099  df-2 9157  df-ndx 13021  df-slot 13022  df-plusg 13109

This theorem is referenced by:  ressplusgd  13148  rngplusgg  13156  srngplusgd  13167  lmodplusgd  13185  ipsaddgd  13197  topgrpplusgd  13217  prdsplusgfval  13303  imasex  13324  imasival  13325  imasbas  13326  imasplusg  13327  imasaddfn  13336  imasaddval  13337  imasaddf  13338  qusaddval  13354  qusaddf  13355  ismgm  13376  plusfvalg  13382  plusffng  13384  gsumpropd2  13412  gsumsplit1r  13417  gsumprval  13418  issgrp  13422  ismnddef  13437  gsumfzz  13514  gsumwsubmcl  13515  gsumwmhm  13517  gsumfzcl  13518  grppropstrg  13538  grpsubval  13565  mulgval  13645  mulgfng  13647  mulgnngsum  13650  mulg1  13652  mulgnnp1  13653  mulgnndir  13674  subgintm  13721  isnsg  13725  gsumfzreidx  13860  gsumfzsubmcl  13861  gsumfzmptfidmadd  13862  gsumfzconst  13864  gsumfzmhm  13866  fnmgp  13871  mgpvalg  13872  mgpplusgg  13873  mgpex  13874  mgpbasg  13875  mgpscag  13876  mgptsetg  13877  mgpdsg  13879  mgpress  13880  isrng  13883  issrg  13914  isring  13949  ring1  14008  oppraddg  14025  islmod  14240  rmodislmod  14300  lsssn0  14319  lss1d  14332  lssintclm  14333  sraaddgg  14389  mpocnfldadd  14510  psrplusgg  14627