# Metamath Proof Explorer

## Theorem 3wlkdlem3

Description: Lemma 3 for 3wlkd . (Contributed by Alexander van der Vekens, 10-Nov-2017) (Revised by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
Assertion 3wlkdlem3 ${⊢}{\phi }\to \left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)$

### Proof

Step Hyp Ref Expression
1 3wlkd.p ${⊢}{P}=⟨“{A}{B}{C}{D}”⟩$
2 3wlkd.f ${⊢}{F}=⟨“{J}{K}{L}”⟩$
3 3wlkd.s ${⊢}{\phi }\to \left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)$
4 1 fveq1i ${⊢}{P}\left(0\right)=⟨“{A}{B}{C}{D}”⟩\left(0\right)$
5 s4fv0 ${⊢}{A}\in {V}\to ⟨“{A}{B}{C}{D}”⟩\left(0\right)={A}$
6 4 5 syl5eq ${⊢}{A}\in {V}\to {P}\left(0\right)={A}$
7 1 fveq1i ${⊢}{P}\left(1\right)=⟨“{A}{B}{C}{D}”⟩\left(1\right)$
8 s4fv1 ${⊢}{B}\in {V}\to ⟨“{A}{B}{C}{D}”⟩\left(1\right)={B}$
9 7 8 syl5eq ${⊢}{B}\in {V}\to {P}\left(1\right)={B}$
10 6 9 anim12i ${⊢}\left({A}\in {V}\wedge {B}\in {V}\right)\to \left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)$
11 1 fveq1i ${⊢}{P}\left(2\right)=⟨“{A}{B}{C}{D}”⟩\left(2\right)$
12 s4fv2 ${⊢}{C}\in {V}\to ⟨“{A}{B}{C}{D}”⟩\left(2\right)={C}$
13 11 12 syl5eq ${⊢}{C}\in {V}\to {P}\left(2\right)={C}$
14 1 fveq1i ${⊢}{P}\left(3\right)=⟨“{A}{B}{C}{D}”⟩\left(3\right)$
15 s4fv3 ${⊢}{D}\in {V}\to ⟨“{A}{B}{C}{D}”⟩\left(3\right)={D}$
16 14 15 syl5eq ${⊢}{D}\in {V}\to {P}\left(3\right)={D}$
17 13 16 anim12i ${⊢}\left({C}\in {V}\wedge {D}\in {V}\right)\to \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)$
18 10 17 anim12i ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({C}\in {V}\wedge {D}\in {V}\right)\right)\to \left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)$
19 3 18 syl ${⊢}{\phi }\to \left(\left({P}\left(0\right)={A}\wedge {P}\left(1\right)={B}\right)\wedge \left({P}\left(2\right)={C}\wedge {P}\left(3\right)={D}\right)\right)$