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	⊢ 𝑆 Struct 𝑋
	strfv.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strfv.n	⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ 𝑆
Assertion	strfv	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strfv.s	⊢ 𝑆 Struct 𝑋
2		strfv.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3		strfv.n	⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ 𝑆
4		structex	⊢ ( 𝑆 Struct 𝑋 → 𝑆 ∈ V )
5	1 4	ax-mp	⊢ 𝑆 ∈ V
6	1	structfun	⊢ Fun ◡ ◡ 𝑆
7		opex	⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ V
8	7	snss	⊢ ( ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 ↔ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ 𝑆 )
9	3 8	mpbir	⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆
10	5 6 2 9	strfv2	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )