Description: Extract a structure component C (such as the base set) from a structure S (such as a member of Poset , df-poset ) with a component extractor E (such as the base set extractor df-base ). By virtue of ndxid , 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)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | strfv.s | |- S Struct X |
|
| strfv.e | |- E = Slot ( E ` ndx ) |
||
| strfv.n | |- { <. ( E ` ndx ) , C >. } C_ S |
||
| Assertion | strfv | |- ( C e. V -> C = ( E ` S ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strfv.s | |- S Struct X |
|
| 2 | strfv.e | |- E = Slot ( E ` ndx ) |
|
| 3 | strfv.n | |- { <. ( E ` ndx ) , C >. } C_ S |
|
| 4 | structex | |- ( S Struct X -> S e. _V ) |
|
| 5 | 1 4 | ax-mp | |- S e. _V |
| 6 | 1 | structfun | |- Fun `' `' S |
| 7 | opex | |- <. ( E ` ndx ) , C >. e. _V |
|
| 8 | 7 | snss | |- ( <. ( E ` ndx ) , C >. e. S <-> { <. ( E ` ndx ) , C >. } C_ S ) |
| 9 | 3 8 | mpbir | |- <. ( E ` ndx ) , C >. e. S |
| 10 | 5 6 2 9 | strfv2 | |- ( C e. V -> C = ( E ` S ) ) |