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