Metamath Proof Explorer

Theorem 2wlkdlem3

Description: Lemma 3 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p ⊢P=⟨“ABC”⟩
2wlkd.f ⊢F=⟨“JK”⟩
2wlkd.s ⊢φ→A∈V∧B∈V∧C∈V
Assertion 2wlkdlem3 ⊢φ→P⁡0=A∧P⁡1=B∧P⁡2=C

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢P=⟨“ABC”⟩
2 2wlkd.f ⊢F=⟨“JK”⟩
3 2wlkd.s ⊢φ→A∈V∧B∈V∧C∈V
4 1 fveq1i ⊢P⁡0=⟨“ABC”⟩⁡0
5 s3fv0 ⊢A∈V→⟨“ABC”⟩⁡0=A
6 4 5 eqtrid ⊢A∈V→P⁡0=A
7 1 fveq1i ⊢P⁡1=⟨“ABC”⟩⁡1
8 s3fv1 ⊢B∈V→⟨“ABC”⟩⁡1=B
9 7 8 eqtrid ⊢B∈V→P⁡1=B
10 1 fveq1i ⊢P⁡2=⟨“ABC”⟩⁡2
11 s3fv2 ⊢C∈V→⟨“ABC”⟩⁡2=C
12 10 11 eqtrid ⊢C∈V→P⁡2=C
13 6 9 12 3anim123i ⊢A∈V∧B∈V∧C∈V→P⁡0=A∧P⁡1=B∧P⁡2=C
14 3 13 syl ⊢φ→P⁡0=A∧P⁡1=B∧P⁡2=C