Metamath Proof Explorer


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 ) )