Step | Hyp | Ref
| Expression |
1 | | 1wlkp1.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | 1wlkp1.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
3 | | 1wlkp1.f |
. . . 4
⊢ (𝜑 → Fun 𝐼) |
4 | | 1wlkp1.a |
. . . 4
⊢ (𝜑 → 𝐼 ∈ Fin) |
5 | | 1wlkp1.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ V) |
6 | | 1wlkp1.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
7 | | 1wlkp1.d |
. . . 4
⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) |
8 | | 1wlkp1.w |
. . . 4
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) |
9 | | 1wlkp1.n |
. . . 4
⊢ 𝑁 = (#‘𝐹) |
10 | | 1wlkp1.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) |
11 | | 1wlkp1.x |
. . . 4
⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) |
12 | | 1wlkp1.u |
. . . 4
⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) |
13 | | 1wlkp1.h |
. . . 4
⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) |
14 | | 1wlkp1.q |
. . . 4
⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) |
15 | | 1wlkp1.s |
. . . 4
⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | 1wlkp1lem6 40887 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) |
17 | 10 | elfvexd 6132 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ V) |
18 | 1, 2 | is1wlkg 40816 |
. . . . . 6
⊢ (𝐺 ∈ V → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) |
20 | 9 | eqcomi 2619 |
. . . . . . . . 9
⊢
(#‘𝐹) = 𝑁 |
21 | 20 | oveq2i 6560 |
. . . . . . . 8
⊢
(0..^(#‘𝐹)) =
(0..^𝑁) |
22 | 21 | raleqi 3119 |
. . . . . . 7
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
23 | 22 | biimpi 205 |
. . . . . 6
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
24 | 23 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
25 | 19, 24 | syl6bi 242 |
. . . 4
⊢ (𝜑 → (𝐹(1Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
26 | 8, 25 | mpd 15 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
27 | | eqeq12 2623 |
. . . . . . 7
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) → ((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)))) |
28 | 27 | 3adant3 1074 |
. . . . . 6
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1)))) |
29 | | simp3 1056 |
. . . . . . 7
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) |
30 | | simp1 1054 |
. . . . . . . 8
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (𝑄‘𝑘) = (𝑃‘𝑘)) |
31 | 30 | sneqd 4137 |
. . . . . . 7
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → {(𝑄‘𝑘)} = {(𝑃‘𝑘)}) |
32 | 29, 31 | eqeq12d 2625 |
. . . . . 6
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)} ↔ (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)})) |
33 | | preq12 4214 |
. . . . . . . 8
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) → {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
34 | 33 | 3adant3 1074 |
. . . . . . 7
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) |
35 | 34, 29 | sseq12d 3597 |
. . . . . 6
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ({(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)) ↔ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
36 | 28, 32, 35 | ifpbi123d 1021 |
. . . . 5
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
37 | 36 | biimprd 237 |
. . . 4
⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))) |
38 | 37 | ral2imi 2931 |
. . 3
⊢
(∀𝑘 ∈
(0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))) |
39 | 16, 26, 38 | sylc 63 |
. 2
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) |
40 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | 1wlkp1lem3 40884 |
. . . . 5
⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵)) |
41 | 40 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵)) |
42 | 5, 10, 7 | 3jca 1235 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∈ V ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼)) |
43 | 42 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → (𝐵 ∈ V ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼)) |
44 | | fsnunfv 6358 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼) → ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵) = 𝐸) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵) = 𝐸) |
46 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑄‘𝑥) = (𝑄‘𝑁)) |
47 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝑃‘𝑥) = (𝑃‘𝑁)) |
48 | 46, 47 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝑄‘𝑥) = (𝑃‘𝑥) ↔ (𝑄‘𝑁) = (𝑃‘𝑁))) |
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | 1wlkp1lem5 40886 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥)) |
50 | 2 | 1wlkf 40819 |
. . . . . . . . . 10
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
51 | | lencl 13179 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ Word dom 𝐼 → (#‘𝐹) ∈
ℕ0) |
52 | 9 | eleq1i 2679 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
↔ (#‘𝐹) ∈
ℕ0) |
53 | | elnn0uz 11601 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
54 | 52, 53 | sylbb1 226 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
ℕ0 → 𝑁 ∈
(ℤ≥‘0)) |
55 | 51, 54 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹 ∈ Word dom 𝐼 → 𝑁 ∈
(ℤ≥‘0)) |
56 | 8, 50, 55 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
57 | 56, 53 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
58 | | nn0fz0 12306 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
59 | 57, 58 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
60 | 48, 49, 59 | rspcdva 3288 |
. . . . . 6
⊢ (𝜑 → (𝑄‘𝑁) = (𝑃‘𝑁)) |
61 | 14 | fveq1i 6104 |
. . . . . . . . . . 11
⊢ (𝑄‘(𝑁 + 1)) = ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1)) |
62 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑁 + 1) ∈ V |
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | 1wlkp1lem1 40882 |
. . . . . . . . . . . 12
⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃) |
64 | | fsnunfv 6358 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ (𝑁 + 1) ∈ dom 𝑃) → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1)) = 𝐶) |
65 | 62, 6, 63, 64 | mp3an2i 1421 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑃 ∪ {〈(𝑁 + 1), 𝐶〉})‘(𝑁 + 1)) = 𝐶) |
66 | 61, 65 | syl5eq 2656 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘(𝑁 + 1)) = 𝐶) |
67 | 66 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ (𝑃‘𝑁) = 𝐶)) |
68 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝑃‘𝑁) = 𝐶 ↔ 𝐶 = (𝑃‘𝑁)) |
69 | 67, 68 | syl6bb 275 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ 𝐶 = (𝑃‘𝑁))) |
70 | | 1wlkp1.l |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) |
71 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝐶 = (𝑃‘𝑁) → {𝐶} = {(𝑃‘𝑁)}) |
72 | 71 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → {𝐶} = {(𝑃‘𝑁)}) |
73 | 70, 72 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {(𝑃‘𝑁)}) |
74 | 73 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 = (𝑃‘𝑁) → 𝐸 = {(𝑃‘𝑁)})) |
75 | 69, 74 | sylbid 229 |
. . . . . . 7
⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑃‘𝑁)})) |
76 | | eqeq1 2614 |
. . . . . . . 8
⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ (𝑃‘𝑁) = (𝑄‘(𝑁 + 1)))) |
77 | | sneq 4135 |
. . . . . . . . 9
⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → {(𝑄‘𝑁)} = {(𝑃‘𝑁)}) |
78 | 77 | eqeq2d 2620 |
. . . . . . . 8
⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → (𝐸 = {(𝑄‘𝑁)} ↔ 𝐸 = {(𝑃‘𝑁)})) |
79 | 76, 78 | imbi12d 333 |
. . . . . . 7
⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → (((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)}) ↔ ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑃‘𝑁)}))) |
80 | 75, 79 | syl5ibrcom 236 |
. . . . . 6
⊢ (𝜑 → ((𝑄‘𝑁) = (𝑃‘𝑁) → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)}))) |
81 | 60, 80 | mpd 15 |
. . . . 5
⊢ (𝜑 → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)})) |
82 | 81 | imp 444 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → 𝐸 = {(𝑄‘𝑁)}) |
83 | 41, 45, 82 | 3eqtrd 2648 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}) |
84 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | 1wlkp1lem7 40888 |
. . . 4
⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))) |
85 | 84 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ¬ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))) |
86 | 83, 85 | ifpimpda 1022 |
. 2
⊢ (𝜑 → if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))) |
87 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | 1wlkp1lem2 40883 |
. . . . . 6
⊢ (𝜑 → (#‘𝐻) = (𝑁 + 1)) |
88 | 87 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^(𝑁 + 1))) |
89 | | fzosplitsn 12442 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
90 | 56, 89 | syl 17 |
. . . . 5
⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
91 | 88, 90 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (0..^(#‘𝐻)) = ((0..^𝑁) ∪ {𝑁})) |
92 | 91 | raleqdv 3121 |
. . 3
⊢ (𝜑 → (∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ ∀𝑘 ∈ ((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))) |
93 | | ralunb 3756 |
. . . 4
⊢
(∀𝑘 ∈
((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))) |
94 | 93 | a1i 11 |
. . 3
⊢ (𝜑 → (∀𝑘 ∈ ((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))) |
95 | | fvex 6113 |
. . . . . 6
⊢
(#‘𝐹) ∈
V |
96 | 9, 95 | eqeltri 2684 |
. . . . 5
⊢ 𝑁 ∈ V |
97 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝑄‘𝑘) = (𝑄‘𝑁)) |
98 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝑘 + 1) = (𝑁 + 1)) |
99 | 98 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑁 + 1))) |
100 | 97, 99 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)) ↔ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1)))) |
101 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝑁 → (𝐻‘𝑘) = (𝐻‘𝑁)) |
102 | 101 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = ((iEdg‘𝑆)‘(𝐻‘𝑁))) |
103 | 97 | sneqd 4137 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → {(𝑄‘𝑘)} = {(𝑄‘𝑁)}) |
104 | 102, 103 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)})) |
105 | 97, 99 | preq12d 4220 |
. . . . . . . 8
⊢ (𝑘 = 𝑁 → {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} = {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))}) |
106 | 105, 102 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → ({(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)) ↔ {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))) |
107 | 100, 104,
106 | ifpbi123d 1021 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))) |
108 | 107 | ralsng 4165 |
. . . . 5
⊢ (𝑁 ∈ V → (∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))) |
109 | 96, 108 | mp1i 13 |
. . . 4
⊢ (𝜑 → (∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))) |
110 | 109 | anbi2d 736 |
. . 3
⊢ (𝜑 → ((∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))))) |
111 | 92, 94, 110 | 3bitrd 293 |
. 2
⊢ (𝜑 → (∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))))) |
112 | 39, 86, 111 | mpbir2and 959 |
1
⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) |