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

Metamath Proof Explorer

Theorem wlkdlem2

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

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

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 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6 fveq2 ⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
7 fvoveq1 ⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) )
8 6 7 preq12d ⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } )
9 2fveq3 ⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
10 8 9 sseq12d ⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
11 10 rspcv ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
12 5 11 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
13 fvex ⊢ ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ V
14 fvex ⊢ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ V
15 13 14 prss ⊢ ( ( ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∧ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
16 nncn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ♯ ‘ 𝐹 ) ∈ ℂ )
17 npcan1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
18 16 17 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
19 18 fveq2d ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
20 19 eleq1d ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
21 20 biimpd ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
22 21 adantld ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∧ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
23 15 22 biimtrrid ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
24 12 23 syld ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
25 4 24 syl5com ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
26 fvex ⊢ ( 𝑃 ‘ 𝑘 ) ∈ V
27 fvex ⊢ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V
28 26 27 prss ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
29 simpl ⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
30 28 29 sylbir ⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
32 31 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
33 4 32 mpd ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
34 25 33 jca ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )