Proof of Theorem rusgranumwlklem3
Step | Hyp | Ref
| Expression |
1 | | rusgranumwlk.w |
. . 3
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
2 | | rusgranumwlk.l |
. . 3
⊢ 𝐿 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦
(#‘{𝑤 ∈ (𝑊‘𝑛) ∣ ((2nd ‘𝑤)‘0) = 𝑣})) |
3 | 1, 2 | rusgranumwlklem2 26477 |
. 2
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ (𝑊‘𝑁) ∣ ((2nd ‘𝑤)‘0) = 𝑃})) |
4 | | eqeq2 2621 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → ((#‘(1st
‘𝑐)) = 𝑛 ↔ (#‘(1st
‘𝑐)) = 𝑁)) |
5 | 4 | rabbidv 3164 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛} = {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁}) |
6 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑉 Walks 𝐸) ∈ V |
7 | 6 | rabex 4740 |
. . . . . . . . . 10
⊢ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ∈ V |
8 | 5, 1, 7 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑊‘𝑁) = {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁}) |
9 | 8 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑤 ∈ (𝑊‘𝑁) ↔ 𝑤 ∈ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁})) |
10 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑤 → (1st ‘𝑐) = (1st ‘𝑤)) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑤 → (#‘(1st ‘𝑐)) = (#‘(1st
‘𝑤))) |
12 | 11 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑐 = 𝑤 → ((#‘(1st
‘𝑐)) = 𝑁 ↔ (#‘(1st
‘𝑤)) = 𝑁)) |
13 | 12 | elrab 3331 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ↔ (𝑤 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑤)) = 𝑁)) |
14 | 9, 13 | syl6bb 275 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (𝑤 ∈ (𝑊‘𝑁) ↔ (𝑤 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑤)) = 𝑁))) |
15 | 14 | adantl 481 |
. . . . . 6
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑤 ∈ (𝑊‘𝑁) ↔ (𝑤 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑤)) = 𝑁))) |
16 | 15 | anbi1d 737 |
. . . . 5
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑤 ∈ (𝑊‘𝑁) ∧ ((2nd ‘𝑤)‘0) = 𝑃) ↔ ((𝑤 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑤)) = 𝑁) ∧ ((2nd
‘𝑤)‘0) = 𝑃))) |
17 | | anass 679 |
. . . . 5
⊢ (((𝑤 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑤)) = 𝑁) ∧ ((2nd
‘𝑤)‘0) = 𝑃) ↔ (𝑤 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃))) |
18 | 16, 17 | syl6bb 275 |
. . . 4
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑤 ∈ (𝑊‘𝑁) ∧ ((2nd ‘𝑤)‘0) = 𝑃) ↔ (𝑤 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) |
19 | 18 | rabbidva2 3162 |
. . 3
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ (𝑊‘𝑁) ∣ ((2nd ‘𝑤)‘0) = 𝑃} = {𝑤 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)}) |
20 | 19 | fveq2d 6107 |
. 2
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(#‘{𝑤 ∈ (𝑊‘𝑁) ∣ ((2nd ‘𝑤)‘0) = 𝑃}) = (#‘{𝑤 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)})) |
21 | 3, 20 | eqtrd 2644 |
1
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑃𝐿𝑁) = (#‘{𝑤 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)})) |