Theorem strss

Description: Propagate component extraction to a structure T from a subset structure S . (Contributed by Mario Carneiro, 11-Oct-2013) (Revised by Mario Carneiro, 15-Jan-2014)

	Ref	Expression
Hypotheses	strss.t	$$⊢T\in \mathrm{V}$$
	strss.f	$$⊢\mathrm{Fun}T$$
	strss.s	$$⊢S\subseteq T$$
	strss.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	strss.n	$$⊢⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
Assertion	strss	$$⊢E\left(T\right)=E\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		strss.t	$$⊢T\in \mathrm{V}$$
2		strss.f	$$⊢\mathrm{Fun}T$$
3		strss.s	$$⊢S\subseteq T$$
4		strss.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
5		strss.n	$$⊢⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
6	1	a1i	$$⊢\top \to T\in \mathrm{V}$$
7	2	a1i	$$⊢\top \to \mathrm{Fun}T$$
8	3	a1i	$$⊢\top \to S\subseteq T$$
9	5	a1i	$$⊢\top \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
10	4 6 7 8 9	strssd	$$⊢\top \to E\left(T\right)=E\left(S\right)$$
11	10	mptru	$$⊢E\left(T\right)=E\left(S\right)$$