This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐼 )