Proof of Theorem 1wlkdlem2
Step | Hyp | Ref
| Expression |
1 | | 1wlkd.e |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) |
2 | | fzo0end 12426 |
. . . . 5
⊢
((#‘𝐹) ∈
ℕ → ((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹))) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = ((#‘𝐹) − 1) → (𝑃‘𝑘) = (𝑃‘((#‘𝐹) − 1))) |
4 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = ((#‘𝐹) − 1) → (𝑘 + 1) = (((#‘𝐹) − 1) + 1)) |
5 | 4 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = ((#‘𝐹) − 1) → (𝑃‘(𝑘 + 1)) = (𝑃‘(((#‘𝐹) − 1) + 1))) |
6 | 3, 5 | preq12d 4220 |
. . . . . . 7
⊢ (𝑘 = ((#‘𝐹) − 1) → {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))}) |
7 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = ((#‘𝐹) − 1) → (𝐹‘𝑘) = (𝐹‘((#‘𝐹) − 1))) |
8 | 7 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑘 = ((#‘𝐹) − 1) → (𝐼‘(𝐹‘𝑘)) = (𝐼‘(𝐹‘((#‘𝐹) − 1)))) |
9 | 6, 8 | sseq12d 3597 |
. . . . . 6
⊢ (𝑘 = ((#‘𝐹) − 1) → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ⊆ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
10 | 9 | rspcv 3278 |
. . . . 5
⊢
(((#‘𝐹)
− 1) ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ⊆ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
11 | 2, 10 | syl 17 |
. . . 4
⊢
((#‘𝐹) ∈
ℕ → (∀𝑘
∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ⊆ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
12 | | fvex 6113 |
. . . . . 6
⊢ (𝑃‘((#‘𝐹) − 1)) ∈
V |
13 | | fvex 6113 |
. . . . . 6
⊢ (𝑃‘(((#‘𝐹) − 1) + 1)) ∈
V |
14 | 12, 13 | prss 4291 |
. . . . 5
⊢ (((𝑃‘((#‘𝐹) − 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))) ∧ (𝑃‘(((#‘𝐹) − 1) + 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1)))) ↔ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ⊆ (𝐼‘(𝐹‘((#‘𝐹) − 1)))) |
15 | | nncn 10905 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℕ → (#‘𝐹)
∈ ℂ) |
16 | | npcan1 10334 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℂ → (((#‘𝐹) − 1) + 1) = (#‘𝐹)) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢
((#‘𝐹) ∈
ℕ → (((#‘𝐹) − 1) + 1) = (#‘𝐹)) |
18 | 17 | fveq2d 6107 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ → (𝑃‘(((#‘𝐹) − 1) + 1)) = (𝑃‘(#‘𝐹))) |
19 | 18 | eleq1d 2672 |
. . . . . . 7
⊢
((#‘𝐹) ∈
ℕ → ((𝑃‘(((#‘𝐹) − 1) + 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))) ↔ (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
20 | 19 | biimpd 218 |
. . . . . 6
⊢
((#‘𝐹) ∈
ℕ → ((𝑃‘(((#‘𝐹) − 1) + 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))) → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
21 | 20 | adantld 482 |
. . . . 5
⊢
((#‘𝐹) ∈
ℕ → (((𝑃‘((#‘𝐹) − 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))) ∧ (𝑃‘(((#‘𝐹) − 1) + 1)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1)))) → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
22 | 14, 21 | syl5bir 232 |
. . . 4
⊢
((#‘𝐹) ∈
ℕ → ({(𝑃‘((#‘𝐹) − 1)), (𝑃‘(((#‘𝐹) − 1) + 1))} ⊆ (𝐼‘(𝐹‘((#‘𝐹) − 1))) → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
23 | 11, 22 | syld 46 |
. . 3
⊢
((#‘𝐹) ∈
ℕ → (∀𝑘
∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
24 | 1, 23 | syl5com 31 |
. 2
⊢ (𝜑 → ((#‘𝐹) ∈ ℕ → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1))))) |
25 | | fvex 6113 |
. . . . . . 7
⊢ (𝑃‘𝑘) ∈ V |
26 | | fvex 6113 |
. . . . . . 7
⊢ (𝑃‘(𝑘 + 1)) ∈ V |
27 | 25, 26 | prss 4291 |
. . . . . 6
⊢ (((𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)) ∧ (𝑃‘(𝑘 + 1)) ∈ (𝐼‘(𝐹‘𝑘))) ↔ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) |
28 | | simpl 472 |
. . . . . 6
⊢ (((𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)) ∧ (𝑃‘(𝑘 + 1)) ∈ (𝐼‘(𝐹‘𝑘))) → (𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))) |
29 | 27, 28 | sylbir 224 |
. . . . 5
⊢ ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → (𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))) |
30 | 29 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^(#‘𝐹))) → ({(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → (𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)))) |
31 | 30 | ralimdva 2945 |
. . 3
⊢ (𝜑 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)))) |
32 | 1, 31 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘))) |
33 | 24, 32 | jca 553 |
1
⊢ (𝜑 → (((#‘𝐹) ∈ ℕ → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)))) |