Metamath Proof Explorer

Theorem wlkdlem1

Description: Lemma 1 for wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses wlkd.p ⊢ φ → P ∈ Word V
wlkd.f ⊢ φ → F ∈ Word V
wlkd.l ⊢ φ → P = F + 1
wlkdlem1.v ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V
Assertion wlkdlem1 ⊢ φ → P : 0 … F ⟶ V

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢ φ → P ∈ Word V
2 wlkd.f ⊢ φ → F ∈ Word V
3 wlkd.l ⊢ φ → P = F + 1
4 wlkdlem1.v ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V
5 wrdf ⊢ P ∈ Word V → P : 0 ..^ P ⟶ V
6 1 5 syl ⊢ φ → P : 0 ..^ P ⟶ V
7 3 oveq2d ⊢ φ → 0 ..^ P = 0 ..^ F + 1
8 lencl ⊢ F ∈ Word V → F ∈ ℕ 0
9 2 8 syl ⊢ φ → F ∈ ℕ 0
10 9 nn0zd ⊢ φ → F ∈ ℤ
11 fzval3 ⊢ F ∈ ℤ → 0 … F = 0 ..^ F + 1
12 10 11 syl ⊢ φ → 0 … F = 0 ..^ F + 1
13 7 12 eqtr4d ⊢ φ → 0 ..^ P = 0 … F
14 13 feq2d ⊢ φ → P : 0 ..^ P ⟶ V ↔ P : 0 … F ⟶ V
15 ssv ⊢ V ⊆ V
16 frnssb ⊢ V ⊆ V ∧ ∀ k ∈ 0 … F P ⁡ k ∈ V → P : 0 … F ⟶ V ↔ P : 0 … F ⟶ V
17 15 4 16 sylancr ⊢ φ → P : 0 … F ⟶ V ↔ P : 0 … F ⟶ V
18 14 17 bitrd ⊢ φ → P : 0 ..^ P ⟶ V ↔ P : 0 … F ⟶ V
19 6 18 mpbid ⊢ φ → P : 0 … F ⟶ V