Step | Hyp | Ref
| Expression |
1 | | wlkop 26056 |
. . . . 5
⊢ (𝐴 ∈ (𝑉 Walks 𝐸) → 𝐴 = ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
2 | | 1st2ndb 7097 |
. . . . 5
⊢ (𝐴 ∈ (V × V) ↔
𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩) |
3 | 1, 2 | sylibr 223 |
. . . 4
⊢ (𝐴 ∈ (𝑉 Walks 𝐸) → 𝐴 ∈ (V × V)) |
4 | | wlkop 26056 |
. . . . 5
⊢ (𝐵 ∈ (𝑉 Walks 𝐸) → 𝐵 = ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
5 | | 1st2ndb 7097 |
. . . . 5
⊢ (𝐵 ∈ (V × V) ↔
𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩) |
6 | 4, 5 | sylibr 223 |
. . . 4
⊢ (𝐵 ∈ (𝑉 Walks 𝐸) → 𝐵 ∈ (V × V)) |
7 | | xpopth 7098 |
. . . . 5
⊢ ((𝐴 ∈ (V × V) ∧
𝐵 ∈ (V × V))
→ (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd} ‘𝐴) = (2^{nd} ‘𝐵)) ↔ 𝐴 = 𝐵)) |
8 | 7 | bicomd 212 |
. . . 4
⊢ ((𝐴 ∈ (V × V) ∧
𝐵 ∈ (V × V))
→ (𝐴 = 𝐵 ↔ ((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴) =
(2^{nd} ‘𝐵)))) |
9 | 3, 6, 8 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) → (𝐴 = 𝐵 ↔ ((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)))) |
10 | 9 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → (𝐴 = 𝐵 ↔ ((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)))) |
11 | | wlkelwrd 26058 |
. . . . . 6
⊢ (𝐴 ∈ (𝑉 Walks 𝐸) → ((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd}
‘𝐴):(0...(#‘(1^{st} ‘𝐴)))⟶𝑉)) |
12 | | wlkelwrd 26058 |
. . . . . 6
⊢ (𝐵 ∈ (𝑉 Walks 𝐸) → ((1^{st} ‘𝐵) ∈ Word dom 𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) |
13 | 11, 12 | anim12i 588 |
. . . . 5
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) → (((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd}
‘𝐴):(0...(#‘(1^{st} ‘𝐴)))⟶𝑉) ∧ ((1^{st} ‘𝐵) ∈ Word dom 𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉))) |
14 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩ →
(𝐴 ∈ (𝑉 Walks 𝐸) ↔ ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ (𝑉 Walks 𝐸))) |
15 | | df-br 4584 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐴)(𝑉 Walks 𝐸)(2^{nd} ‘𝐴) ↔ ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ (𝑉 Walks 𝐸)) |
16 | | wlklenvm1 26060 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐴)(𝑉 Walks 𝐸)(2^{nd} ‘𝐴) → (#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1)) |
17 | 15, 16 | sylbir 224 |
. . . . . . . 8
⊢
(⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1)) |
18 | 14, 17 | syl6bi 242 |
. . . . . . 7
⊢ (𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩ →
(𝐴 ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1))) |
19 | 1, 18 | mpcom 37 |
. . . . . 6
⊢ (𝐴 ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1)) |
20 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩ →
(𝐵 ∈ (𝑉 Walks 𝐸) ↔ ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈ (𝑉 Walks 𝐸))) |
21 | | df-br 4584 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐵)(𝑉 Walks 𝐸)(2^{nd} ‘𝐵) ↔ ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈ (𝑉 Walks 𝐸)) |
22 | | wlklenvm1 26060 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐵)(𝑉 Walks 𝐸)(2^{nd} ‘𝐵) → (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1)) |
23 | 21, 22 | sylbir 224 |
. . . . . . . 8
⊢
(⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1)) |
24 | 20, 23 | syl6bi 242 |
. . . . . . 7
⊢ (𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩ →
(𝐵 ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) |
25 | 4, 24 | mpcom 37 |
. . . . . 6
⊢ (𝐵 ∈ (𝑉 Walks 𝐸) → (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1)) |
26 | 19, 25 | anim12i 588 |
. . . . 5
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) → ((#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1) ∧ (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) |
27 | | eqwrd 13201 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (1^{st} ‘𝐵) ∈ Word dom 𝐸) → ((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ↔
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)))) |
28 | 27 | ad2ant2r 779 |
. . . . . . 7
⊢
((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) → ((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ↔
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)))) |
29 | 28 | adantr 480 |
. . . . . 6
⊢
(((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) ∧ ((#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1) ∧ (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) → ((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ↔
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)))) |
30 | | lencl 13179 |
. . . . . . . . . . 11
⊢
((1^{st} ‘𝐴) ∈ Word dom 𝐸 → (#‘(1^{st}
‘𝐴)) ∈
ℕ_{0}) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢
(((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) →
(#‘(1^{st} ‘𝐴)) ∈
ℕ_{0}) |
32 | 31 | adantr 480 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) → (#‘(1^{st}
‘𝐴)) ∈
ℕ_{0}) |
33 | | simplr 788 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) → (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) |
34 | | simprr 792 |
. . . . . . . . 9
⊢
((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) → (2^{nd} ‘𝐵):(0...(#‘(1^{st}
‘𝐵)))⟶𝑉) |
35 | 32, 33, 34 | 3jca 1235 |
. . . . . . . 8
⊢
((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) → ((#‘(1^{st}
‘𝐴)) ∈
ℕ_{0} ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st} ‘𝐴)))⟶𝑉 ∧ (2^{nd} ‘𝐵):(0...(#‘(1^{st}
‘𝐵)))⟶𝑉)) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢
(((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) ∧ ((#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1) ∧ (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) →
((#‘(1^{st} ‘𝐴)) ∈ ℕ_{0} ∧
(2^{nd} ‘𝐴):(0...(#‘(1^{st} ‘𝐴)))⟶𝑉 ∧ (2^{nd} ‘𝐵):(0...(#‘(1^{st}
‘𝐵)))⟶𝑉)) |
37 | | 2ffzeq 12329 |
. . . . . . 7
⊢
(((#‘(1^{st} ‘𝐴)) ∈ ℕ_{0} ∧
(2^{nd} ‘𝐴):(0...(#‘(1^{st} ‘𝐴)))⟶𝑉 ∧ (2^{nd} ‘𝐵):(0...(#‘(1^{st}
‘𝐵)))⟶𝑉) → ((2^{nd}
‘𝐴) = (2^{nd}
‘𝐵) ↔
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
38 | 36, 37 | syl 17 |
. . . . . 6
⊢
(((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) ∧ ((#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1) ∧ (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) → ((2^{nd}
‘𝐴) = (2^{nd}
‘𝐵) ↔
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
39 | 29, 38 | anbi12d 743 |
. . . . 5
⊢
(((((1^{st} ‘𝐴) ∈ Word dom 𝐸 ∧ (2^{nd} ‘𝐴):(0...(#‘(1^{st}
‘𝐴)))⟶𝑉) ∧ ((1^{st}
‘𝐵) ∈ Word dom
𝐸 ∧ (2^{nd}
‘𝐵):(0...(#‘(1^{st} ‘𝐵)))⟶𝑉)) ∧ ((#‘(1^{st}
‘𝐴)) =
((#‘(2^{nd} ‘𝐴)) − 1) ∧ (#‘(1^{st}
‘𝐵)) =
((#‘(2^{nd} ‘𝐵)) − 1))) → (((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴) =
(2^{nd} ‘𝐵))
↔ (((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥))))) |
40 | 13, 26, 39 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸)) → (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)) ↔
(((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥))))) |
41 | 40 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → (((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴) =
(2^{nd} ‘𝐵))
↔ (((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥))))) |
42 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) → (𝑁 = (#‘(1^{st}
‘𝐵)) ↔
(#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)))) |
43 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) →
(0..^𝑁) =
(0..^(#‘(1^{st} ‘𝐴)))) |
44 | 43 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) →
(∀𝑥 ∈
(0..^𝑁)((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥) ↔ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥))) |
45 | 42, 44 | anbi12d 743 |
. . . . . 6
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) → ((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ↔ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(#‘(1^{st}
‘𝐴)))((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥)))) |
46 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) →
(0...𝑁) =
(0...(#‘(1^{st} ‘𝐴)))) |
47 | 46 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) →
(∀𝑥 ∈
(0...𝑁)((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥) ↔ ∀𝑥 ∈
(0...(#‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) |
48 | 42, 47 | anbi12d 743 |
. . . . . 6
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) → ((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)) ↔ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥)))) |
49 | 45, 48 | anbi12d 743 |
. . . . 5
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) → (((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) ↔ (((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(#‘(1^{st}
‘𝐴)))((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥)) ∧
((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0...(#‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))))) |
50 | 49 | bibi2d 331 |
. . . 4
⊢ (𝑁 = (#‘(1^{st}
‘𝐴)) →
((((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd} ‘𝐴) = (2^{nd} ‘𝐵)) ↔ ((𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) ↔ (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)) ↔
(((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥)))))) |
51 | 50 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → ((((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴) =
(2^{nd} ‘𝐵))
↔ ((𝑁 =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) ↔ (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)) ↔
(((#‘(1^{st} ‘𝐴)) = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈
(0..^(#‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ ((#‘(1^{st}
‘𝐴)) =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(#‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥)))))) |
52 | 41, 51 | mpbird 246 |
. 2
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → (((1^{st}
‘𝐴) = (1^{st}
‘𝐵) ∧
(2^{nd} ‘𝐴) =
(2^{nd} ‘𝐵))
↔ ((𝑁 =
(#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))))) |
53 | | 3anass 1035 |
. . . 4
⊢ ((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)) ↔ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ (∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
54 | | anandi 867 |
. . . 4
⊢ ((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
(∀𝑥 ∈
(0..^𝑁)((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) ↔ ((𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
55 | 53, 54 | bitr2i 264 |
. . 3
⊢ (((𝑁 = (#‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) ↔ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) |
56 | 55 | a1i 11 |
. 2
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → (((𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ∧ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥))) ↔ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
57 | 10, 52, 56 | 3bitrd 293 |
1
⊢ ((𝐴 ∈ (𝑉 Walks 𝐸) ∧ 𝐵 ∈ (𝑉 Walks 𝐸) ∧ 𝑁 = (#‘(1^{st} ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |