wlkdlem3

	Ref	Expression
Hypotheses	wlkd.p	$⊢ φ \to P \in Word V$
	wlkd.f	$⊢ φ \to F \in Word V$
	wlkd.l	$⊢ φ \to \|P\| = \|F\| + 1$
	wlkd.e	$⊢ φ \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
Assertion	wlkdlem3	$⊢ φ \to F \in Word dom I$

Step	Hyp	Ref	Expression
1		wlkd.p	$⊢ φ \to P \in Word V$
2		wlkd.f	$⊢ φ \to F \in Word V$
3		wlkd.l	$⊢ φ \to \|P\| = \|F\| + 1$
4		wlkd.e	$⊢ φ \to \forall k \in (0 ..^\|F\|) \{P (k), P (k + 1)\} \subseteq I (F (k))$
5	1 2 3 4	wlkdlem2	$⊢ φ \to ((\|F\| \in ℕ \to P (\|F\|) \in I (F (\|F\| - 1))) \land \forall k \in (0 ..^\|F\|) P (k) \in I (F (k)))$
6		elfvdm	$⊢ P (k) \in I (F (k)) \to F (k) \in dom I$
7	6	ralimi	$⊢ \forall k \in (0 ..^\|F\|) P (k) \in I (F (k)) \to \forall k \in (0 ..^\|F\|) F (k) \in dom I$
8	5 7	simpl2im	$⊢ φ \to \forall k \in (0 ..^\|F\|) F (k) \in dom I$
9		iswrdsymb	$⊢ (F \in Word V \land \forall k \in (0 ..^\|F\|) F (k) \in dom I) \to F \in Word dom I$
10	2 8 9	syl2anc	$⊢ φ \to F \in Word dom I$

Metamath Proof Explorer