2wlkdlem7

	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	2wlkdlem7	$⊢ φ \to (J \in V \land K \in V)$

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	2wlkdlem6	$⊢ φ \to (B \in I (J) \land B \in I (K))$
7		elfvex	$⊢ B \in I (J) \to J \in V$
8		elfvex	$⊢ B \in I (K) \to K \in V$
9	7 8	anim12i	$⊢ (B \in I (J) \land B \in I (K)) \to (J \in V \land K \in V)$
10	6 9	syl	$⊢ φ \to (J \in V \land K \in V)$

Metamath Proof Explorer