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\leftrightarrow \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)$$