Proof of Theorem rusgranumwlkb0
Step | Hyp | Ref
| Expression |
1 | | 0nn0 11184 |
. . 3
⊢ 0 ∈
ℕ0 |
2 | | rusgranumwlk.w |
. . . 4
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
3 | | rusgranumwlk.l |
. . . 4
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) |
4 | 2, 3 | rusgranumwlklem4 26479 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 0 ∈ ℕ0) →
(𝑃𝐿0) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃})) |
5 | 1, 4 | mp3an3 1405 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃})) |
6 | | df-rab 2905 |
. . . . 5
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∧ (𝑤‘0) = 𝑃)} |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∧ (𝑤‘0) = 𝑃)}) |
8 | | usgrav 25867 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
10 | | wwlkn0s 26233 |
. . . . . . . . 9
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1}) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → ((𝑉 WWalksN 𝐸)‘0) = {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1}) |
12 | 11 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ↔ 𝑤 ∈ {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1})) |
13 | | rabid 3095 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 1} ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1)) |
14 | 12, 13 | syl6bb 275 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ↔ (𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1))) |
15 | 14 | anbi1d 737 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃))) |
16 | 15 | abbidv 2728 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∣ (𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∧ (𝑤‘0) = 𝑃)} = {𝑤 ∣ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)}) |
17 | | wrdl1s1 13247 |
. . . . . . . 8
⊢ (𝑃 ∈ 𝑉 → (𝑣 = 〈“𝑃”〉 ↔ (𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1 ∧ (𝑣‘0) = 𝑃))) |
18 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1 ∧ (𝑣‘0) = 𝑃) ↔ ((𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃)) |
19 | 17, 18 | syl6rbb 276 |
. . . . . . 7
⊢ (𝑃 ∈ 𝑉 → (((𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃) ↔ 𝑣 = 〈“𝑃”〉)) |
20 | | vex 3176 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
21 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑣 → (𝑤 ∈ Word 𝑉 ↔ 𝑣 ∈ Word 𝑉)) |
22 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (#‘𝑤) = (#‘𝑣)) |
23 | 22 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑣 → ((#‘𝑤) = 1 ↔ (#‘𝑣) = 1)) |
24 | 21, 23 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑤 = 𝑣 → ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ↔ (𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1))) |
25 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑣 → (𝑤‘0) = (𝑣‘0)) |
26 | 25 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑤 = 𝑣 → ((𝑤‘0) = 𝑃 ↔ (𝑣‘0) = 𝑃)) |
27 | 24, 26 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑤 = 𝑣 → (((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃))) |
28 | 20, 27 | elab 3319 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑤 ∣ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} ↔ ((𝑣 ∈ Word 𝑉 ∧ (#‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃)) |
29 | | velsn 4141 |
. . . . . . 7
⊢ (𝑣 ∈ {〈“𝑃”〉} ↔ 𝑣 = 〈“𝑃”〉) |
30 | 19, 28, 29 | 3bitr4g 302 |
. . . . . 6
⊢ (𝑃 ∈ 𝑉 → (𝑣 ∈ {𝑤 ∣ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} ↔ 𝑣 ∈ {〈“𝑃”〉})) |
31 | 30 | eqrdv 2608 |
. . . . 5
⊢ (𝑃 ∈ 𝑉 → {𝑤 ∣ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} = {〈“𝑃”〉}) |
32 | 31 | adantl 481 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∣ ((𝑤 ∈ Word 𝑉 ∧ (#‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} = {〈“𝑃”〉}) |
33 | 7, 16, 32 | 3eqtrd 2648 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃} = {〈“𝑃”〉}) |
34 | 33 | fveq2d 6107 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (#‘{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘0) ∣ (𝑤‘0) = 𝑃}) = (#‘{〈“𝑃”〉})) |
35 | | s1cl 13235 |
. . . 4
⊢ (𝑃 ∈ 𝑉 → 〈“𝑃”〉 ∈ Word 𝑉) |
36 | | hashsng 13020 |
. . . 4
⊢
(〈“𝑃”〉 ∈ Word 𝑉 → (#‘{〈“𝑃”〉}) =
1) |
37 | 35, 36 | syl 17 |
. . 3
⊢ (𝑃 ∈ 𝑉 → (#‘{〈“𝑃”〉}) =
1) |
38 | 37 | adantl 481 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (#‘{〈“𝑃”〉}) =
1) |
39 | 5, 34, 38 | 3eqtrd 2648 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) |