# Metamath Proof Explorer

## Theorem strfv

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}\mathrm{Struct}{X}$
strfv.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
strfv.n ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\subseteq {S}$
Assertion strfv ${⊢}{C}\in {V}\to {C}={E}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 strfv.s ${⊢}{S}\mathrm{Struct}{X}$
2 strfv.e ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
3 strfv.n ${⊢}\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\subseteq {S}$
4 structex ${⊢}{S}\mathrm{Struct}{X}\to {S}\in \mathrm{V}$
5 1 4 ax-mp ${⊢}{S}\in \mathrm{V}$
6 1 structfun ${⊢}\mathrm{Fun}{{{S}}^{-1}}^{-1}$
7 opex ${⊢}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in \mathrm{V}$
8 7 snss ${⊢}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in {S}↔\left\{⟨{E}\left(\mathrm{ndx}\right),{C}⟩\right\}\subseteq {S}$
9 3 8 mpbir ${⊢}⟨{E}\left(\mathrm{ndx}\right),{C}⟩\in {S}$
10 5 6 2 9 strfv2 ${⊢}{C}\in {V}\to {C}={E}\left({S}\right)$