MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  strfv Structured version   Unicode version

Theorem strfv 14693
Description: Extract a structure component  C (such as the base set) from a structure  S (such as a member of  Poset, df-poset 15715) with a component extractor  E (such as the base set extractor df-base 14662). By virtue of ndxid 14678, this can be done without having to refer to the hard-coded numeric index of 
E. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.)
Hypotheses
Ref Expression
strfv.s  |-  S Struct  X
strfv.e  |-  E  = Slot  ( E `  ndx )
strfv.n  |-  { <. ( E `  ndx ) ,  C >. }  C_  S
Assertion
Ref Expression
strfv  |-  ( C  e.  V  ->  C  =  ( E `  S ) )

Proof of Theorem strfv
StepHypRef Expression
1 strfv.s . . 3  |-  S Struct  X
2 brstruct 14665 . . . 4  |-  Rel Struct
32brrelexi 4971 . . 3  |-  ( S Struct  X  ->  S  e.  _V )
41, 3ax-mp 5 . 2  |-  S  e. 
_V
51structfun 14669 . 2  |-  Fun  `' `' S
6 strfv.e . 2  |-  E  = Slot  ( E `  ndx )
7 strfv.n . . 3  |-  { <. ( E `  ndx ) ,  C >. }  C_  S
8 opex 4643 . . . 4  |-  <. ( E `  ndx ) ,  C >.  e.  _V
98snss 4085 . . 3  |-  ( <.
( E `  ndx ) ,  C >.  e.  S  <->  { <. ( E `  ndx ) ,  C >. } 
C_  S )
107, 9mpbir 209 . 2  |-  <. ( E `  ndx ) ,  C >.  e.  S
114, 5, 6, 10strfv2 14692 1  |-  ( C  e.  V  ->  C  =  ( E `  S ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1836   _Vcvv 3051    C_ wss 3406   {csn 3961   <.cop 3967   class class class wbr 4384   ` cfv 5513   Struct cstr 14653   ndxcnx 14654  Slot cslot 14656
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-n0 10735  df-z 10804  df-uz 11024  df-fz 11616  df-struct 14659  df-slot 14661
This theorem is referenced by:  strfv3  14694  1strbas  14762  2strbas  14766  2strop  14767  rngbase  14777  rngplusg  14778  rngmulr  14779  srngbase  14785  srngplusg  14786  srngmulr  14787  srnginvl  14788  lmodbase  14794  lmodplusg  14795  lmodsca  14796  lmodvsca  14797  ipsbase  14801  ipsaddg  14802  ipsmulr  14803  ipssca  14804  ipsvsca  14805  ipsip  14806  phlbase  14811  phlplusg  14812  phlsca  14813  phlvsca  14814  phlip  14815  topgrpbas  14819  topgrpplusg  14820  topgrptset  14821  otpsbas  14826  otpstset  14827  otpsle  14828  odrngbas  14837  odrngplusg  14838  odrngmulr  14839  odrngtset  14840  odrngle  14841  odrngds  14842  imassca  14949  imastset  14952  fuccofval  15388  setcbas  15497  catchomfval  15517  catccofval  15519  estrcbas  15534  ipobas  15925  ipolerval  15926  ipotset  15927  psrbas  18166  psrbasOLD  18167  psrplusg  18170  psrmulr  18173  psrsca  18178  psrvscafval  18179  cnfldbas  18560  cnfldadd  18561  cnfldmul  18562  cnfldcj  18563  cnfldtset  18564  cnfldle  18565  cnfldds  18566  cnfldunif  18567  trkgbas  23981  trkgdist  23982  trkgitv  23983  algbase  31335  algaddg  31336  algmulr  31337  algsca  31338  algvsca  31339  rngchomfvalALTV  33031  rngccofvalALTV  33034  ringchomfvalALTV  33094  ringccofvalALTV  33097
  Copyright terms: Public domain W3C validator