Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . 6
⊢ ((𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁) →
(#‘(1st ‘𝑊)) = 𝑁) |
2 | 1 | eqcomd 2616 |
. . . . 5
⊢ ((𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁) → 𝑁 = (#‘(1st ‘𝑊))) |
3 | 2 | 3ad2ant3 1077 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → 𝑁 = (#‘(1st ‘𝑊))) |
4 | 3 | adantr 480 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → 𝑁 = (#‘(1st
‘𝑊))) |
5 | | fveq1 6102 |
. . . . 5
⊢
((2nd ‘𝑋) = (2nd ‘𝑊) → ((2nd ‘𝑋)‘𝑖) = ((2nd ‘𝑊)‘𝑖)) |
6 | 5 | adantl 481 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) →
((2nd ‘𝑋)‘𝑖) = ((2nd ‘𝑊)‘𝑖)) |
7 | 6 | ralrimivw 2950 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) →
∀𝑖 ∈ (0...𝑁)((2nd ‘𝑋)‘𝑖) = ((2nd ‘𝑊)‘𝑖)) |
8 | | simpl1l 1105 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → 𝑉 USGrph 𝐸) |
9 | | simpl 472 |
. . . . . . 7
⊢ ((𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) → 𝑋 ∈ (𝑉 Walks 𝐸)) |
10 | | simpl 472 |
. . . . . . 7
⊢ ((𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁) → 𝑊 ∈ (𝑉 Walks 𝐸)) |
11 | 9, 10 | anim12i 588 |
. . . . . 6
⊢ (((𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → (𝑋 ∈ (𝑉 Walks 𝐸) ∧ 𝑊 ∈ (𝑉 Walks 𝐸))) |
12 | 11 | 3adant1 1072 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → (𝑋 ∈ (𝑉 Walks 𝐸) ∧ 𝑊 ∈ (𝑉 Walks 𝐸))) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → (𝑋 ∈ (𝑉 Walks 𝐸) ∧ 𝑊 ∈ (𝑉 Walks 𝐸))) |
14 | | simpr 476 |
. . . . . . 7
⊢ ((𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) →
(#‘(1st ‘𝑋)) = 𝑁) |
15 | 14 | eqcomd 2616 |
. . . . . 6
⊢ ((𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) → 𝑁 = (#‘(1st ‘𝑋))) |
16 | 15 | 3ad2ant2 1076 |
. . . . 5
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → 𝑁 = (#‘(1st ‘𝑋))) |
17 | 16 | adantr 480 |
. . . 4
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → 𝑁 = (#‘(1st
‘𝑋))) |
18 | | usg2wlkeq 26236 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ 𝑊 ∈ (𝑉 Walks 𝐸)) ∧ 𝑁 = (#‘(1st ‘𝑋))) → (𝑋 = 𝑊 ↔ (𝑁 = (#‘(1st ‘𝑊)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑋)‘𝑖) = ((2nd ‘𝑊)‘𝑖)))) |
19 | 8, 13, 17, 18 | syl3anc 1318 |
. . 3
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → (𝑋 = 𝑊 ↔ (𝑁 = (#‘(1st ‘𝑊)) ∧ ∀𝑖 ∈ (0...𝑁)((2nd ‘𝑋)‘𝑖) = ((2nd ‘𝑊)‘𝑖)))) |
20 | 4, 7, 19 | mpbir2and 959 |
. 2
⊢ ((((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) ∧ (2nd
‘𝑋) = (2nd
‘𝑊)) → 𝑋 = 𝑊) |
21 | 20 | ex 449 |
1
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) ∧ (𝑋 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑋)) = 𝑁) ∧ (𝑊 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑊)) = 𝑁)) → ((2nd
‘𝑋) = (2nd
‘𝑊) → 𝑋 = 𝑊)) |