Step | Hyp | Ref
| Expression |
1 | | 1wlkd.f |
. . . . . . . . . 10
⊢ 𝐹 = ⟨“𝐽”⟩ |
2 | 1 | fveq1i 6892 |
. . . . . . . . 9
⊢ (𝐹‘0) = (⟨“𝐽”⟩‘0) |
3 | | 1wlkd.p |
. . . . . . . . . . . 12
⊢ 𝑃 = ⟨“𝑋𝑌”⟩ |
4 | | 1wlkd.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
5 | | 1wlkd.y |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
6 | | 1wlkd.l |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) |
7 | | 1wlkd.j |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) |
8 | 3, 1, 4, 5, 6, 7 | 1wlkdlem2 29388 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽)) |
9 | 8 | elfvexd 6930 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ V) |
10 | | s1fv 14559 |
. . . . . . . . . 10
⊢ (𝐽 ∈ V →
(⟨“𝐽”⟩‘0) = 𝐽) |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (⟨“𝐽”⟩‘0) = 𝐽) |
12 | 2, 11 | eqtrid 2784 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘0) = 𝐽) |
13 | 12 | fveq2d 6895 |
. . . . . . 7
⊢ (𝜑 → (𝐼‘(𝐹‘0)) = (𝐼‘𝐽)) |
14 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘(𝐹‘0)) = (𝐼‘𝐽)) |
15 | 14, 6 | eqtrd 2772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘(𝐹‘0)) = {𝑋}) |
16 | | df-ne 2941 |
. . . . . . 7
⊢ (𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌) |
17 | 16, 7 | sylan2br 595 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) |
18 | 13 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑌) → (𝐼‘(𝐹‘0)) = (𝐼‘𝐽)) |
19 | 17, 18 | sseqtrrd 4023 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑋 = 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘(𝐹‘0))) |
20 | 15, 19 | ifpimpda 1081 |
. . . 4
⊢ (𝜑 → if-(𝑋 = 𝑌, (𝐼‘(𝐹‘0)) = {𝑋}, {𝑋, 𝑌} ⊆ (𝐼‘(𝐹‘0)))) |
21 | 3 | fveq1i 6892 |
. . . . . 6
⊢ (𝑃‘0) = (⟨“𝑋𝑌”⟩‘0) |
22 | | s2fv0 14837 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (⟨“𝑋𝑌”⟩‘0) = 𝑋) |
23 | 4, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → (⟨“𝑋𝑌”⟩‘0) = 𝑋) |
24 | 21, 23 | eqtrid 2784 |
. . . . 5
⊢ (𝜑 → (𝑃‘0) = 𝑋) |
25 | 3 | fveq1i 6892 |
. . . . . 6
⊢ (𝑃‘1) = (⟨“𝑋𝑌”⟩‘1) |
26 | | s2fv1 14838 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → (⟨“𝑋𝑌”⟩‘1) = 𝑌) |
27 | 5, 26 | syl 17 |
. . . . . 6
⊢ (𝜑 → (⟨“𝑋𝑌”⟩‘1) = 𝑌) |
28 | 25, 27 | eqtrid 2784 |
. . . . 5
⊢ (𝜑 → (𝑃‘1) = 𝑌) |
29 | | eqeq12 2749 |
. . . . . 6
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → ((𝑃‘0) = (𝑃‘1) ↔ 𝑋 = 𝑌)) |
30 | | sneq 4638 |
. . . . . . . 8
⊢ ((𝑃‘0) = 𝑋 → {(𝑃‘0)} = {𝑋}) |
31 | 30 | adantr 481 |
. . . . . . 7
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → {(𝑃‘0)} = {𝑋}) |
32 | 31 | eqeq2d 2743 |
. . . . . 6
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → ((𝐼‘(𝐹‘0)) = {(𝑃‘0)} ↔ (𝐼‘(𝐹‘0)) = {𝑋})) |
33 | | preq12 4739 |
. . . . . . 7
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → {(𝑃‘0), (𝑃‘1)} = {𝑋, 𝑌}) |
34 | 33 | sseq1d 4013 |
. . . . . 6
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → ({(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)) ↔ {𝑋, 𝑌} ⊆ (𝐼‘(𝐹‘0)))) |
35 | 29, 32, 34 | ifpbi123d 1078 |
. . . . 5
⊢ (((𝑃‘0) = 𝑋 ∧ (𝑃‘1) = 𝑌) → (if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-(𝑋 = 𝑌, (𝐼‘(𝐹‘0)) = {𝑋}, {𝑋, 𝑌} ⊆ (𝐼‘(𝐹‘0))))) |
36 | 24, 28, 35 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))) ↔ if-(𝑋 = 𝑌, (𝐼‘(𝐹‘0)) = {𝑋}, {𝑋, 𝑌} ⊆ (𝐼‘(𝐹‘0))))) |
37 | 20, 36 | mpbird 256 |
. . 3
⊢ (𝜑 → if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
38 | | c0ex 11207 |
. . . 4
⊢ 0 ∈
V |
39 | | oveq1 7415 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
40 | | 0p1e1 12333 |
. . . . . 6
⊢ (0 + 1) =
1 |
41 | 39, 40 | eqtrdi 2788 |
. . . . 5
⊢ (𝑘 = 0 → (𝑘 + 1) = 1) |
42 | | wkslem2 28862 |
. . . . 5
⊢ ((𝑘 = 0 ∧ (𝑘 + 1) = 1) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
43 | 41, 42 | mpdan 685 |
. . . 4
⊢ (𝑘 = 0 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0))))) |
44 | 38, 43 | ralsn 4685 |
. . 3
⊢
(∀𝑘 ∈
{0}if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘0) = (𝑃‘1), (𝐼‘(𝐹‘0)) = {(𝑃‘0)}, {(𝑃‘0), (𝑃‘1)} ⊆ (𝐼‘(𝐹‘0)))) |
45 | 37, 44 | sylibr 233 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ {0}if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
46 | 1 | fveq2i 6894 |
. . . . . . 7
⊢
(♯‘𝐹) =
(♯‘⟨“𝐽”⟩) |
47 | | s1len 14555 |
. . . . . . 7
⊢
(♯‘⟨“𝐽”⟩) = 1 |
48 | 46, 47 | eqtri 2760 |
. . . . . 6
⊢
(♯‘𝐹) =
1 |
49 | 48 | oveq2i 7419 |
. . . . 5
⊢
(0..^(♯‘𝐹)) = (0..^1) |
50 | | fzo01 13713 |
. . . . 5
⊢ (0..^1) =
{0} |
51 | 49, 50 | eqtri 2760 |
. . . 4
⊢
(0..^(♯‘𝐹)) = {0} |
52 | 51 | a1i 11 |
. . 3
⊢ (𝜑 → (0..^(♯‘𝐹)) = {0}) |
53 | 52 | raleqdv 3325 |
. 2
⊢ (𝜑 → (∀𝑘 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ ∀𝑘 ∈ {0}if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
54 | 45, 53 | mpbird 256 |
1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |