Theorem strfv2d

Description: Deduction version of strfv2 . (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	strfv2d.e	|- E = Slot ( E ` ndx )
	strfv2d.s	|- ( ph -> S e. V )
	strfv2d.f	|- ( ph -> Fun `' `' S )
	strfv2d.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
	strfv2d.c	|- ( ph -> C e. W )
Assertion	strfv2d	|- ( ph -> C = ( E ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strfv2d.e	|- E = Slot ( E ` ndx )
2		strfv2d.s	|- ( ph -> S e. V )
3		strfv2d.f	|- ( ph -> Fun `' `' S )
4		strfv2d.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
5		strfv2d.c	|- ( ph -> C e. W )
6	1 2	strfvnd	|- ( ph -> ( E ` S ) = ( S ` ( E ` ndx ) ) )
7		cnvcnv2	|- `' `' S = ( S |` _V )
8	7	fveq1i	|- ( `' `' S ` ( E ` ndx ) ) = ( ( S |` _V ) ` ( E ` ndx ) )
9		fvex	|- ( E ` ndx ) e. _V
10		fvres	|- ( ( E ` ndx ) e. _V -> ( ( S |` _V ) ` ( E ` ndx ) ) = ( S ` ( E ` ndx ) ) )
11	9 10	ax-mp	|- ( ( S |` _V ) ` ( E ` ndx ) ) = ( S ` ( E ` ndx ) )
12	8 11	eqtri	|- ( `' `' S ` ( E ` ndx ) ) = ( S ` ( E ` ndx ) )
13	5	elexd	|- ( ph -> C e. _V )
14		opelxpi	|- ( ( ( E ` ndx ) e. _V /\ C e. _V ) -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
15	9 13 14	sylancr	|- ( ph -> <. ( E ` ndx ) , C >. e. ( _V X. _V ) )
16	4 15	elind	|- ( ph -> <. ( E ` ndx ) , C >. e. ( S i^i ( _V X. _V ) ) )
17		cnvcnv	|- `' `' S = ( S i^i ( _V X. _V ) )
18	16 17	eleqtrrdi	|- ( ph -> <. ( E ` ndx ) , C >. e. `' `' S )
19		funopfv	|- ( Fun `' `' S -> ( <. ( E ` ndx ) , C >. e. `' `' S -> ( `' `' S ` ( E ` ndx ) ) = C ) )
20	3 18 19	sylc	|- ( ph -> ( `' `' S ` ( E ` ndx ) ) = C )
21	12 20	eqtr3id	|- ( ph -> ( S ` ( E ` ndx ) ) = C )
22	6 21	eqtr2d	|- ( ph -> C = ( E ` S ) )