3wlkdlem8

	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))$
	3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
	3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
Assertion	3wlkdlem8	$⊢ φ \to (F (0) = J \land F (1) = K \land F (2) = L)$

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		3wlkd.n	$⊢ φ \to ((A \neq B \land A \neq C) \land (B \neq C \land B \neq D) \land C \neq D)$
5		3wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K) \land \{C, D\} \subseteq I (L))$
6	1 2 3 4 5	3wlkdlem7	$⊢ φ \to (J \in V \land K \in V \land L \in V)$
7		s3fv0	$⊢ J \in V \to ⟨“ J K L ”⟩ (0) = J$
8		s3fv1	$⊢ K \in V \to ⟨“ J K L ”⟩ (1) = K$
9		s3fv2	$⊢ L \in V \to ⟨“ J K L ”⟩ (2) = L$
10	7 8 9	3anim123i	$⊢ (J \in V \land K \in V \land L \in V) \to (⟨“ J K L ”⟩ (0) = J \land ⟨“ J K L ”⟩ (1) = K \land ⟨“ J K L ”⟩ (2) = L)$
11	6 10	syl	$⊢ φ \to (⟨“ J K L ”⟩ (0) = J \land ⟨“ J K L ”⟩ (1) = K \land ⟨“ J K L ”⟩ (2) = L)$
12	2	fveq1i	$⊢ F (0) = ⟨“ J K L ”⟩ (0)$
13	12	eqeq1i	$⊢ F (0) = J \leftrightarrow ⟨“ J K L ”⟩ (0) = J$
14	2	fveq1i	$⊢ F (1) = ⟨“ J K L ”⟩ (1)$
15	14	eqeq1i	$⊢ F (1) = K \leftrightarrow ⟨“ J K L ”⟩ (1) = K$
16	2	fveq1i	$⊢ F (2) = ⟨“ J K L ”⟩ (2)$
17	16	eqeq1i	$⊢ F (2) = L \leftrightarrow ⟨“ J K L ”⟩ (2) = L$
18	13 15 17	3anbi123i	$⊢ (F (0) = J \land F (1) = K \land F (2) = L) \leftrightarrow (⟨“ J K L ”⟩ (0) = J \land ⟨“ J K L ”⟩ (1) = K \land ⟨“ J K L ”⟩ (2) = L)$
19	11 18	sylibr	$⊢ φ \to (F (0) = J \land F (1) = K \land F (2) = L)$

Metamath Proof Explorer