Theorem wlkdlem3

Description: Lemma 3 for wlkd . (Contributed by Alexander van der Vekens, 10-Nov-2017) (Revised by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
	wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
	wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
	wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion	wlkdlem3	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
2		wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
3		wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
4		wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
5	1 2 3 4	wlkdlem2	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
6		elfvdm	⊢ ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 )
7	6	ralimi	⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 )
8	5 7	simpl2im	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 )
9		iswrdsymb	⊢ ( ( 𝐹 ∈ Word V ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐹 ‘ 𝑘 ) ∈ dom 𝐼 ) → 𝐹 ∈ Word dom 𝐼 )
10	2 8 9	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )