Metamath Proof Explorer

Theorem wlkdlem2

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

Ref Expression
Hypotheses wlkd.p ⊢φ→P∈WordV
wlkd.f ⊢φ→F∈WordV
wlkd.l ⊢φ→P=F+1
wlkd.e ⊢φ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k
Assertion wlkdlem2 ⊢φ→F∈ℕ→P⁡F∈I⁡F⁡F−1∧∀k∈0..^FP⁡k∈I⁡F⁡k

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢φ→P∈WordV
2 wlkd.f ⊢φ→F∈WordV
3 wlkd.l ⊢φ→P=F+1
4 wlkd.e ⊢φ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k
5 fzo0end ⊢F∈ℕ→F−1∈0..^F
6 fveq2 ⊢k=F−1→P⁡k=P⁡F−1
7 fvoveq1 ⊢k=F−1→P⁡k+1=P⁡F-1+1
8 6 7 preq12d ⊢k=F−1→P⁡kP⁡k+1=P⁡F−1P⁡F-1+1
9 2fveq3 ⊢k=F−1→I⁡F⁡k=I⁡F⁡F−1
10 8 9 sseq12d ⊢k=F−1→P⁡kP⁡k+1⊆I⁡F⁡k↔P⁡F−1P⁡F-1+1⊆I⁡F⁡F−1
11 10 rspcv ⊢F−1∈0..^F→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k→P⁡F−1P⁡F-1+1⊆I⁡F⁡F−1
12 5 11 syl ⊢F∈ℕ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k→P⁡F−1P⁡F-1+1⊆I⁡F⁡F−1
13 fvex ⊢P⁡F−1∈V
14 fvex ⊢P⁡F-1+1∈V
15 13 14 prss ⊢P⁡F−1∈I⁡F⁡F−1∧P⁡F-1+1∈I⁡F⁡F−1↔P⁡F−1P⁡F-1+1⊆I⁡F⁡F−1
16 nncn ⊢F∈ℕ→F∈ℂ
17 npcan1 ⊢F∈ℂ→F-1+1=F
18 16 17 syl ⊢F∈ℕ→F-1+1=F
19 18 fveq2d ⊢F∈ℕ→P⁡F-1+1=P⁡F
20 19 eleq1d ⊢F∈ℕ→P⁡F-1+1∈I⁡F⁡F−1↔P⁡F∈I⁡F⁡F−1
21 20 biimpd ⊢F∈ℕ→P⁡F-1+1∈I⁡F⁡F−1→P⁡F∈I⁡F⁡F−1
22 21 adantld ⊢F∈ℕ→P⁡F−1∈I⁡F⁡F−1∧P⁡F-1+1∈I⁡F⁡F−1→P⁡F∈I⁡F⁡F−1
23 15 22 biimtrrid ⊢F∈ℕ→P⁡F−1P⁡F-1+1⊆I⁡F⁡F−1→P⁡F∈I⁡F⁡F−1
24 12 23 syld ⊢F∈ℕ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k→P⁡F∈I⁡F⁡F−1
25 4 24 syl5com ⊢φ→F∈ℕ→P⁡F∈I⁡F⁡F−1
26 fvex ⊢P⁡k∈V
27 fvex ⊢P⁡k+1∈V
28 26 27 prss ⊢P⁡k∈I⁡F⁡k∧P⁡k+1∈I⁡F⁡k↔P⁡kP⁡k+1⊆I⁡F⁡k
29 simpl ⊢P⁡k∈I⁡F⁡k∧P⁡k+1∈I⁡F⁡k→P⁡k∈I⁡F⁡k
30 28 29 sylbir ⊢P⁡kP⁡k+1⊆I⁡F⁡k→P⁡k∈I⁡F⁡k
31 30 a1i ⊢φ∧k∈0..^F→P⁡kP⁡k+1⊆I⁡F⁡k→P⁡k∈I⁡F⁡k
32 31 ralimdva ⊢φ→∀k∈0..^FP⁡kP⁡k+1⊆I⁡F⁡k→∀k∈0..^FP⁡k∈I⁡F⁡k
33 4 32 mpd ⊢φ→∀k∈0..^FP⁡k∈I⁡F⁡k
34 25 33 jca ⊢φ→F∈ℕ→P⁡F∈I⁡F⁡F−1∧∀k∈0..^FP⁡k∈I⁡F⁡k