Step |
Hyp |
Ref |
Expression |
1 |
|
2wlkd.p |
|- P = <" A B C "> |
2 |
|
2wlkd.f |
|- F = <" J K "> |
3 |
|
2wlkd.s |
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) ) |
4 |
1
|
fveq1i |
|- ( P ` 0 ) = ( <" A B C "> ` 0 ) |
5 |
|
s3fv0 |
|- ( A e. V -> ( <" A B C "> ` 0 ) = A ) |
6 |
4 5
|
eqtrid |
|- ( A e. V -> ( P ` 0 ) = A ) |
7 |
1
|
fveq1i |
|- ( P ` 1 ) = ( <" A B C "> ` 1 ) |
8 |
|
s3fv1 |
|- ( B e. V -> ( <" A B C "> ` 1 ) = B ) |
9 |
7 8
|
eqtrid |
|- ( B e. V -> ( P ` 1 ) = B ) |
10 |
1
|
fveq1i |
|- ( P ` 2 ) = ( <" A B C "> ` 2 ) |
11 |
|
s3fv2 |
|- ( C e. V -> ( <" A B C "> ` 2 ) = C ) |
12 |
10 11
|
eqtrid |
|- ( C e. V -> ( P ` 2 ) = C ) |
13 |
6 9 12
|
3anim123i |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) |
14 |
3 13
|
syl |
|- ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) |