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 = ⟨“ ABCD ”⟩
3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
Assertion 3wlkdlem3 ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
2 3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3 3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
4 1 fveq1i ⊢ P ⁡ 0 = ⟨“ ABCD ”⟩ ⁡ 0
5 s4fv0 ⊢ A ∈ V → ⟨“ ABCD ”⟩ ⁡ 0 = A
6 4 5 syl5eq ⊢ A ∈ V → P ⁡ 0 = A
7 1 fveq1i ⊢ P ⁡ 1 = ⟨“ ABCD ”⟩ ⁡ 1
8 s4fv1 ⊢ B ∈ V → ⟨“ ABCD ”⟩ ⁡ 1 = B
9 7 8 syl5eq ⊢ B ∈ V → P ⁡ 1 = B
10 6 9 anim12i ⊢ A ∈ V ∧ B ∈ V → P ⁡ 0 = A ∧ P ⁡ 1 = B
11 1 fveq1i ⊢ P ⁡ 2 = ⟨“ ABCD ”⟩ ⁡ 2
12 s4fv2 ⊢ C ∈ V → ⟨“ ABCD ”⟩ ⁡ 2 = C
13 11 12 syl5eq ⊢ C ∈ V → P ⁡ 2 = C
14 1 fveq1i ⊢ P ⁡ 3 = ⟨“ ABCD ”⟩ ⁡ 3
15 s4fv3 ⊢ D ∈ V → ⟨“ ABCD ”⟩ ⁡ 3 = D
16 14 15 syl5eq ⊢ D ∈ V → P ⁡ 3 = D
17 13 16 anim12i ⊢ C ∈ V ∧ D ∈ V → P ⁡ 2 = C ∧ P ⁡ 3 = D
18 10 17 anim12i ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D
19 3 18 syl ⊢ φ → P ⁡ 0 = A ∧ P ⁡ 1 = B ∧ P ⁡ 2 = C ∧ P ⁡ 3 = D