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

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 ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
Assertion 3wlkdlem3 ( 𝜑 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
2 3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3 3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
4 1 fveq1i ⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 0 )
5 s4fv0 ⊢ ( 𝐴 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 0 ) = 𝐴 )
6 4 5 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑃 ‘ 0 ) = 𝐴 )
7 1 fveq1i ⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 1 )
8 s4fv1 ⊢ ( 𝐵 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 1 ) = 𝐵 )
9 7 8 eqtrid ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑃 ‘ 1 ) = 𝐵 )
10 6 9 anim12i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) )
11 1 fveq1i ⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 2 )
12 s4fv2 ⊢ ( 𝐶 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 2 ) = 𝐶 )
13 11 12 eqtrid ⊢ ( 𝐶 ∈ 𝑉 → ( 𝑃 ‘ 2 ) = 𝐶 )
14 1 fveq1i ⊢ ( 𝑃 ‘ 3 ) = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 )
15 s4fv3 ⊢ ( 𝐷 ∈ 𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩ ‘ 3 ) = 𝐷 )
16 14 15 eqtrid ⊢ ( 𝐷 ∈ 𝑉 → ( 𝑃 ‘ 3 ) = 𝐷 )
17 13 16 anim12i ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) )
18 10 17 anim12i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) )
19 3 18 syl ⊢ ( 𝜑 → ( ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ) ∧ ( ( 𝑃 ‘ 2 ) = 𝐶 ∧ ( 𝑃 ‘ 3 ) = 𝐷 ) ) )