Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
2 | 1 | anim2i 591 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
3 | 2 | adantl 481 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑋 ∈ 𝑉 ∧ 𝑁 ∈
ℕ0)) |
4 | | numclwwlk.c |
. . . . 5
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
5 | | numclwwlk.f |
. . . . 5
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
6 | | numclwwlk.g |
. . . . 5
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
7 | | numclwwlk.q |
. . . . 5
⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)}) |
8 | 4, 5, 6, 7 | numclwwlkovq 26626 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
9 | 3, 8 | syl 17 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑋𝑄𝑁) = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) |
10 | 9 | fveq2d 6107 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘(𝑋𝑄𝑁)) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})) |
11 | | eqid 2610 |
. . 3
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} |
12 | | eqid 2610 |
. . 3
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} |
13 | 11, 12 | clwlknclwlkdifnum 26488 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}) = ((𝐾↑𝑁) − (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}))) |
14 | | fvex 6113 |
. . . . . 6
⊢ ((𝑉 WWalksN 𝐸)‘𝑁) ∈ V |
15 | 14 | rabex 4740 |
. . . . 5
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} ∈ V |
16 | | rusisusgra 26458 |
. . . . . . . . 9
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → 𝑉 USGrph 𝐸) |
17 | | usgrav 25867 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
18 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑉 ∈ V) |
19 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝐸 ∈ V) |
20 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝐸 ∈ V) |
21 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ) |
22 | 21 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑁 ∈ ℕ) |
23 | 18, 20, 22 | 3jca 1235 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ)) |
24 | 23 | ex 449 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ))) |
25 | 16, 17, 24 | 3syl 18 |
. . . . . . . 8
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ))) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢
((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ))) |
27 | 26 | imp 444 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ)) |
28 | | clwwlkvbij 26329 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ) →
∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
29 | 27, 28 | syl 17 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
30 | | hasheqf1oi 13002 |
. . . . 5
⊢ ({𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)} ∈ V → (∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) = (#‘{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}))) |
31 | 15, 29, 30 | mpsyl 66 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) = (#‘{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋})) |
32 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) |
33 | 32 | adantl 481 |
. . . . . . 7
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑁 ∈
ℕ0) |
34 | 4 | numclwwlkfvc 26604 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
35 | | rabeq 3166 |
. . . . . . 7
⊢ ((𝐶‘𝑁) = ((𝑉 ClWWalksN 𝐸)‘𝑁) → {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
37 | 36 | eqcomd 2616 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → {𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
38 | 37 | fveq2d 6107 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) = (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋})) |
39 | 4, 5 | numclwwlkovf 26608 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑋𝐹𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
40 | 3, 39 | syl 17 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑋𝐹𝑁) = {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
41 | 40 | eqcomd 2616 |
. . . . 5
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → {𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋} = (𝑋𝐹𝑁)) |
42 | 41 | fveq2d 6107 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ (𝐶‘𝑁) ∣ (𝑤‘0) = 𝑋}) = (#‘(𝑋𝐹𝑁))) |
43 | 31, 38, 42 | 3eqtrd 2648 |
. . 3
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}) = (#‘(𝑋𝐹𝑁))) |
44 | 43 | oveq2d 6565 |
. 2
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝐾↑𝑁) − (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)})) = ((𝐾↑𝑁) − (#‘(𝑋𝐹𝑁)))) |
45 | 10, 13, 44 | 3eqtrd 2648 |
1
⊢
(((〈𝑉, 𝐸〉 RegUSGrph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (#‘(𝑋𝑄𝑁)) = ((𝐾↑𝑁) − (#‘(𝑋𝐹𝑁)))) |