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