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 e. _V
	strss.f	|- Fun T
	strss.s	|- S C_ T
	strss.e	|- E = Slot ( E ` ndx )
	strss.n	|- <. ( E ` ndx ) , C >. e. S
Assertion	strss	|- ( E ` T ) = ( E ` S )

Proof

Step	Hyp	Ref	Expression
1		strss.t	|- T e. _V
2		strss.f	|- Fun T
3		strss.s	|- S C_ T
4		strss.e	|- E = Slot ( E ` ndx )
5		strss.n	|- <. ( E ` ndx ) , C >. e. S
6	1	a1i	|- ( T. -> T e. _V )
7	2	a1i	|- ( T. -> Fun T )
8	3	a1i	|- ( T. -> S C_ T )
9	5	a1i	|- ( T. -> <. ( E ` ndx ) , C >. e. S )
10	4 6 7 8 9	strssd	|- ( T. -> ( E ` T ) = ( E ` S ) )
11	10	mptru	|- ( E ` T ) = ( E ` S )