Proof of Theorem rusgrnumwwlkb0
| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → 𝑃 ∈ 𝑉) |
| 2 | | 0nn0 12541 |
. . 3
⊢ 0 ∈
ℕ0 |
| 3 | | rusgrnumwwlk.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
| 4 | | rusgrnumwwlk.l |
. . . 4
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(♯‘{𝑤 ∈
(𝑛 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑣})) |
| 5 | 3, 4 | rusgrnumwwlklem 29990 |
. . 3
⊢ ((𝑃 ∈ 𝑉 ∧ 0 ∈ ℕ0) →
(𝑃𝐿0) = (♯‘{𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃})) |
| 6 | 1, 2, 5 | sylancl 586 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = (♯‘{𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃})) |
| 7 | | df-rab 3437 |
. . . . 5
⊢ {𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∣ (𝑤 ∈ (0 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃)} |
| 8 | 7 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∣ (𝑤 ∈ (0 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃)}) |
| 9 | | wwlksn0s 29881 |
. . . . . . . . 9
⊢ (0
WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1} |
| 10 | 9 | a1i 11 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (0 WWalksN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1}) |
| 11 | 10 | eleq2d 2827 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ (0 WWalksN 𝐺) ↔ 𝑤 ∈ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1})) |
| 12 | | rabid 3458 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑤 ∈ Word (Vtx‘𝐺) ∣ (♯‘𝑤) = 1} ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1)) |
| 13 | 11, 12 | bitrdi 287 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ (0 WWalksN 𝐺) ↔ (𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1))) |
| 14 | 13 | anbi1d 631 |
. . . . 5
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ (0 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃))) |
| 15 | 14 | abbidv 2808 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → {𝑤 ∣ (𝑤 ∈ (0 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃)} = {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)}) |
| 16 | | wrdl1s1 14652 |
. . . . . . . . 9
⊢ (𝑃 ∈ (Vtx‘𝐺) → (𝑣 = 〈“𝑃”〉 ↔ (𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1 ∧ (𝑣‘0) = 𝑃))) |
| 17 | | df-3an 1089 |
. . . . . . . . 9
⊢ ((𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1 ∧ (𝑣‘0) = 𝑃) ↔ ((𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃)) |
| 18 | 16, 17 | bitr2di 288 |
. . . . . . . 8
⊢ (𝑃 ∈ (Vtx‘𝐺) → (((𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃) ↔ 𝑣 = 〈“𝑃”〉)) |
| 19 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
| 20 | | eleq1w 2824 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (𝑤 ∈ Word (Vtx‘𝐺) ↔ 𝑣 ∈ Word (Vtx‘𝐺))) |
| 21 | | fveqeq2 6915 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → ((♯‘𝑤) = 1 ↔ (♯‘𝑣) = 1)) |
| 22 | 20, 21 | anbi12d 632 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑣 → ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ↔ (𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1))) |
| 23 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (𝑤‘0) = (𝑣‘0)) |
| 24 | 23 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑣 → ((𝑤‘0) = 𝑃 ↔ (𝑣‘0) = 𝑃)) |
| 25 | 22, 24 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑤 = 𝑣 → (((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃))) |
| 26 | 19, 25 | elab 3679 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} ↔ ((𝑣 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑣) = 1) ∧ (𝑣‘0) = 𝑃)) |
| 27 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑣 ∈ {〈“𝑃”〉} ↔ 𝑣 = 〈“𝑃”〉) |
| 28 | 18, 26, 27 | 3bitr4g 314 |
. . . . . . 7
⊢ (𝑃 ∈ (Vtx‘𝐺) → (𝑣 ∈ {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} ↔ 𝑣 ∈ {〈“𝑃”〉})) |
| 29 | 28, 3 | eleq2s 2859 |
. . . . . 6
⊢ (𝑃 ∈ 𝑉 → (𝑣 ∈ {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} ↔ 𝑣 ∈ {〈“𝑃”〉})) |
| 30 | 29 | eqrdv 2735 |
. . . . 5
⊢ (𝑃 ∈ 𝑉 → {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} = {〈“𝑃”〉}) |
| 31 | 30 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → {𝑤 ∣ ((𝑤 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑤) = 1) ∧ (𝑤‘0) = 𝑃)} = {〈“𝑃”〉}) |
| 32 | 8, 15, 31 | 3eqtrd 2781 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {〈“𝑃”〉}) |
| 33 | 32 | fveq2d 6910 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ (0 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{〈“𝑃”〉})) |
| 34 | | s1cl 14640 |
. . . 4
⊢ (𝑃 ∈ 𝑉 → 〈“𝑃”〉 ∈ Word 𝑉) |
| 35 | | hashsng 14408 |
. . . 4
⊢
(〈“𝑃”〉 ∈ Word 𝑉 → (♯‘{〈“𝑃”〉}) =
1) |
| 36 | 34, 35 | syl 17 |
. . 3
⊢ (𝑃 ∈ 𝑉 → (♯‘{〈“𝑃”〉}) =
1) |
| 37 | 36 | adantl 481 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (♯‘{〈“𝑃”〉}) =
1) |
| 38 | 6, 33, 37 | 3eqtrd 2781 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉) → (𝑃𝐿0) = 1) |