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 ⊢ φ → P ∈ Word V
wlkd.f ⊢ φ → F ∈ Word V
wlkd.l ⊢ φ → P = F + 1
wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
Assertion wlkdlem3 ⊢ φ → F ∈ Word dom ⁡ I

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢ φ → P ∈ Word V
2 wlkd.f ⊢ φ → F ∈ Word V
3 wlkd.l ⊢ φ → P = F + 1
4 wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 1 2 3 4 wlkdlem2 ⊢ φ → F ∈ ℕ → P ⁡ F ∈ I ⁡ F ⁡ F − 1 ∧ ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k
6 elfvdm ⊢ P ⁡ k ∈ I ⁡ F ⁡ k → F ⁡ k ∈ dom ⁡ I
7 6 ralimi ⊢ ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F F ⁡ k ∈ dom ⁡ I
8 5 7 simpl2im ⊢ φ → ∀ k ∈ 0 ..^ F F ⁡ k ∈ dom ⁡ I
9 iswrdsymb ⊢ F ∈ Word V ∧ ∀ k ∈ 0 ..^ F F ⁡ k ∈ dom ⁡ I → F ∈ Word dom ⁡ I
10 2 8 9 syl2anc ⊢ φ → F ∈ Word dom ⁡ I