Proof of Theorem rusgranumwlklem1
Step | Hyp | Ref
| Expression |
1 | | rusgranumwlk.w |
. . 3
⊢ 𝑊 = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛}) |
2 | | ovex 6577 |
. . . 4
⊢ (𝑉 Walks 𝐸) ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑉 Walks 𝐸) ∈ V) |
4 | 1, 3 | elfvmptrab 6214 |
. 2
⊢ (𝑅 ∈ (𝑊‘𝑁) → (𝑁 ∈ ℕ0 ∧ 𝑅 ∈ (𝑉 Walks 𝐸))) |
5 | 2 | rabex 4740 |
. . . . . . 7
⊢ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ∈ V |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑅 ∈ (𝑉 Walks 𝐸) → {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ∈ V) |
7 | | eqeq2 2621 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → ((#‘(1st
‘𝑐)) = 𝑛 ↔ (#‘(1st
‘𝑐)) = 𝑁)) |
8 | 7 | rabbidv 3164 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑛} = {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁}) |
9 | 8, 1 | fvmptg 6189 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ∈ V) → (𝑊‘𝑁) = {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁}) |
10 | 6, 9 | sylan2 490 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → (𝑊‘𝑁) = {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁}) |
11 | 10 | eleq2d 2673 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → (𝑅 ∈ (𝑊‘𝑁) ↔ 𝑅 ∈ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁})) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑐 = 𝑅 → (1st ‘𝑐) = (1st ‘𝑅)) |
13 | 12 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑐 = 𝑅 → (#‘(1st
‘𝑐)) =
(#‘(1st ‘𝑅))) |
14 | 13 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑐 = 𝑅 → ((#‘(1st
‘𝑐)) = 𝑁 ↔ (#‘(1st
‘𝑅)) = 𝑁)) |
15 | 14 | elrab 3331 |
. . . . 5
⊢ (𝑅 ∈ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} ↔ (𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑅)) = 𝑁)) |
16 | | simpr 476 |
. . . . . 6
⊢ ((𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑅)) = 𝑁) →
(#‘(1st ‘𝑅)) = 𝑁) |
17 | 16 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → ((𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑅)) = 𝑁) →
(#‘(1st ‘𝑅)) = 𝑁)) |
18 | 15, 17 | syl5bi 231 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → (𝑅 ∈ {𝑐 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑐)) = 𝑁} →
(#‘(1st ‘𝑅)) = 𝑁)) |
19 | 11, 18 | sylbid 229 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → (𝑅 ∈ (𝑊‘𝑁) → (#‘(1st
‘𝑅)) = 𝑁)) |
20 | | simpr 476 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → 𝑅 ∈ (𝑉 Walks 𝐸)) |
21 | 19, 20 | jctild 564 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑅 ∈ (𝑉 Walks 𝐸)) → (𝑅 ∈ (𝑊‘𝑁) → (𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑅)) = 𝑁))) |
22 | 4, 21 | mpcom 37 |
1
⊢ (𝑅 ∈ (𝑊‘𝑁) → (𝑅 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑅)) = 𝑁)) |