3wlkdlem3

	Ref	Expression
Hypotheses	3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
	3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
	3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
Assertion	3wlkdlem3	$⊢ φ \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$

Step	Hyp	Ref	Expression
1		3wlkd.p	$⊢ P = ⟨“ A B C D ”⟩$
2		3wlkd.f	$⊢ F = ⟨“ J K L ”⟩$
3		3wlkd.s	$⊢ φ \to ((A \in V \land B \in V) \land (C \in V \land D \in V))$
4	1	fveq1i	$⊢ P (0) = ⟨“ A B C D ”⟩ (0)$
5		s4fv0	$⊢ A \in V \to ⟨“ A B C D ”⟩ (0) = A$
6	4 5	eqtrid	$⊢ A \in V \to P (0) = A$
7	1	fveq1i	$⊢ P (1) = ⟨“ A B C D ”⟩ (1)$
8		s4fv1	$⊢ B \in V \to ⟨“ A B C D ”⟩ (1) = B$
9	7 8	eqtrid	$⊢ B \in V \to P (1) = B$
10	6 9	anim12i	$⊢ (A \in V \land B \in V) \to (P (0) = A \land P (1) = B)$
11	1	fveq1i	$⊢ P (2) = ⟨“ A B C D ”⟩ (2)$
12		s4fv2	$⊢ C \in V \to ⟨“ A B C D ”⟩ (2) = C$
13	11 12	eqtrid	$⊢ C \in V \to P (2) = C$
14	1	fveq1i	$⊢ P (3) = ⟨“ A B C D ”⟩ (3)$
15		s4fv3	$⊢ D \in V \to ⟨“ A B C D ”⟩ (3) = D$
16	14 15	eqtrid	$⊢ D \in V \to P (3) = D$
17	13 16	anim12i	$⊢ (C \in V \land D \in V) \to (P (2) = C \land P (3) = D)$
18	10 17	anim12i	$⊢ ((A \in V \land B \in V) \land (C \in V \land D \in V)) \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$
19	3 18	syl	$⊢ φ \to ((P (0) = A \land P (1) = B) \land (P (2) = C \land P (3) = D))$

Metamath Proof Explorer