This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2wlkdlem3

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

Ref Expression
Hypotheses 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
Assertion 2wlkdlem3 ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 2wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) )
4 1 fveq1i ⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 )
5 s3fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
6 4 5 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝐴 )
7 1 fveq1i ⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 )
8 s3fv1 ⊢ ( 𝐵 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
9 7 8 eqtrid ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑃 ‘ 1 ) = 𝐵 )
10 1 fveq1i ⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 )
11 s3fv2 ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
12 10 11 eqtrid ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑃 ‘ 2 ) = 𝐶 )
13 6 9 12 3anim123i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )
14 3 13 syl ⊢ ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )