2wlkdlem8

	Ref	Expression
Hypotheses	2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
	2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
	2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
	2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
	2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
Assertion	2wlkdlem8	$⊢ φ \to (F (0) = J \land F (1) = K)$

Step	Hyp	Ref	Expression
1		2wlkd.p	$⊢ P = ⟨“ A B C ”⟩$
2		2wlkd.f	$⊢ F = ⟨“ J K ”⟩$
3		2wlkd.s	$⊢ φ \to (A \in V \land B \in V \land C \in V)$
4		2wlkd.n	$⊢ φ \to (A \neq B \land B \neq C)$
5		2wlkd.e	$⊢ φ \to (\{A, B\} \subseteq I (J) \land \{B, C\} \subseteq I (K))$
6	1 2 3 4 5	2wlkdlem7	$⊢ φ \to (J \in V \land K \in V)$
7		s2fv0	$⊢ J \in V \to ⟨“ J K ”⟩ (0) = J$
8		s2fv1	$⊢ K \in V \to ⟨“ J K ”⟩ (1) = K$
9	7 8	anim12i	$⊢ (J \in V \land K \in V) \to (⟨“ J K ”⟩ (0) = J \land ⟨“ J K ”⟩ (1) = K)$
10	6 9	syl	$⊢ φ \to (⟨“ J K ”⟩ (0) = J \land ⟨“ J K ”⟩ (1) = K)$
11	2	fveq1i	$⊢ F (0) = ⟨“ J K ”⟩ (0)$
12	11	eqeq1i	$⊢ F (0) = J \leftrightarrow ⟨“ J K ”⟩ (0) = J$
13	2	fveq1i	$⊢ F (1) = ⟨“ J K ”⟩ (1)$
14	13	eqeq1i	$⊢ F (1) = K \leftrightarrow ⟨“ J K ”⟩ (1) = K$
15	12 14	anbi12i	$⊢ (F (0) = J \land F (1) = K) \leftrightarrow (⟨“ J K ”⟩ (0) = J \land ⟨“ J K ”⟩ (1) = K)$
16	10 15	sylibr	$⊢ φ \to (F (0) = J \land F (1) = K)$

Metamath Proof Explorer