Step | Hyp | Ref
| Expression |
1 | | eqid 2798 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2798 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
3 | | eqid 2798 |
. . . . . . 7
⊢
(1^{st} ‘𝐴) = (1^{st} ‘𝐴) |
4 | | eqid 2798 |
. . . . . . 7
⊢
(2^{nd} ‘𝐴) = (2^{nd} ‘𝐴) |
5 | 1, 2, 3, 4 | wlkelwrd 27432 |
. . . . . 6
⊢ (𝐴 ∈ (Walks‘𝐺) → ((1^{st}
‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺))) |
6 | | eqid 2798 |
. . . . . . 7
⊢
(1^{st} ‘𝐵) = (1^{st} ‘𝐵) |
7 | | eqid 2798 |
. . . . . . 7
⊢
(2^{nd} ‘𝐵) = (2^{nd} ‘𝐵) |
8 | 1, 2, 6, 7 | wlkelwrd 27432 |
. . . . . 6
⊢ (𝐵 ∈ (Walks‘𝐺) → ((1^{st}
‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) |
9 | 5, 8 | anim12i 615 |
. . . . 5
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (((1^{st} ‘𝐴) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺)))) |
10 | | wlkop 27427 |
. . . . . . 7
⊢ (𝐴 ∈ (Walks‘𝐺) → 𝐴 = ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩) |
11 | | eleq1 2877 |
. . . . . . . 8
⊢ (𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩ →
(𝐴 ∈
(Walks‘𝐺) ↔
⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ (Walks‘𝐺))) |
12 | | df-br 5032 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐴)(Walks‘𝐺)(2^{nd} ‘𝐴) ↔ ⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈
(Walks‘𝐺)) |
13 | | wlklenvm1 27421 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐴)(Walks‘𝐺)(2^{nd} ‘𝐴) → (♯‘(1^{st}
‘𝐴)) =
((♯‘(2^{nd} ‘𝐴)) − 1)) |
14 | 12, 13 | sylbir 238 |
. . . . . . . 8
⊢
(⟨(1^{st} ‘𝐴), (2^{nd} ‘𝐴)⟩ ∈ (Walks‘𝐺) →
(♯‘(1^{st} ‘𝐴)) = ((♯‘(2^{nd}
‘𝐴)) −
1)) |
15 | 11, 14 | syl6bi 256 |
. . . . . . 7
⊢ (𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩ →
(𝐴 ∈
(Walks‘𝐺) →
(♯‘(1^{st} ‘𝐴)) = ((♯‘(2^{nd}
‘𝐴)) −
1))) |
16 | 10, 15 | mpcom 38 |
. . . . . 6
⊢ (𝐴 ∈ (Walks‘𝐺) →
(♯‘(1^{st} ‘𝐴)) = ((♯‘(2^{nd}
‘𝐴)) −
1)) |
17 | | wlkop 27427 |
. . . . . . 7
⊢ (𝐵 ∈ (Walks‘𝐺) → 𝐵 = ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩) |
18 | | eleq1 2877 |
. . . . . . . 8
⊢ (𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩ →
(𝐵 ∈
(Walks‘𝐺) ↔
⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈ (Walks‘𝐺))) |
19 | | df-br 5032 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐵)(Walks‘𝐺)(2^{nd} ‘𝐵) ↔ ⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈
(Walks‘𝐺)) |
20 | | wlklenvm1 27421 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐵)(Walks‘𝐺)(2^{nd} ‘𝐵) → (♯‘(1^{st}
‘𝐵)) =
((♯‘(2^{nd} ‘𝐵)) − 1)) |
21 | 19, 20 | sylbir 238 |
. . . . . . . 8
⊢
(⟨(1^{st} ‘𝐵), (2^{nd} ‘𝐵)⟩ ∈ (Walks‘𝐺) →
(♯‘(1^{st} ‘𝐵)) = ((♯‘(2^{nd}
‘𝐵)) −
1)) |
22 | 18, 21 | syl6bi 256 |
. . . . . . 7
⊢ (𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩ →
(𝐵 ∈
(Walks‘𝐺) →
(♯‘(1^{st} ‘𝐵)) = ((♯‘(2^{nd}
‘𝐵)) −
1))) |
23 | 17, 22 | mpcom 38 |
. . . . . 6
⊢ (𝐵 ∈ (Walks‘𝐺) →
(♯‘(1^{st} ‘𝐵)) = ((♯‘(2^{nd}
‘𝐵)) −
1)) |
24 | 16, 23 | anim12i 615 |
. . . . 5
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → ((♯‘(1^{st}
‘𝐴)) =
((♯‘(2^{nd} ‘𝐴)) − 1) ∧
(♯‘(1^{st} ‘𝐵)) = ((♯‘(2^{nd}
‘𝐵)) −
1))) |
25 | | eqwrd 13903 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (1^{st}
‘𝐵) ∈ Word dom
(iEdg‘𝐺)) →
((1^{st} ‘𝐴)
= (1^{st} ‘𝐵)
↔ ((♯‘(1^{st} ‘𝐴)) = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈
(0..^(♯‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)))) |
26 | 25 | ad2ant2r 746 |
. . . . . . 7
⊢
((((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) → ((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ↔
((♯‘(1^{st} ‘𝐴)) = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈
(0..^(♯‘(1^{st} ‘𝐴)))((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)))) |
27 | 26 | adantr 484 |
. . . . . 6
⊢
(((((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) ∧ ((♯‘(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}
‘𝐵)‘𝑥)))) |
28 | | lencl 13879 |
. . . . . . . . 9
⊢
((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) →
(♯‘(1^{st} ‘𝐴)) ∈
ℕ_{0}) |
29 | 28 | adantr 484 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) → (♯‘(1^{st}
‘𝐴)) ∈
ℕ_{0}) |
30 | | simpr 488 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) → (2^{nd} ‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) |
31 | | simpr 488 |
. . . . . . . 8
⊢
(((1^{st} ‘𝐵) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺)) → (2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺)) |
32 | | 2ffzeq 13026 |
. . . . . . . 8
⊢
(((♯‘(1^{st} ‘𝐴)) ∈ ℕ_{0} ∧
(2^{nd} ‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺) ∧ (2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺)) → ((2^{nd} ‘𝐴) = (2^{nd} ‘𝐵) ↔
((♯‘(1^{st} ‘𝐴)) = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈
(0...(♯‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
33 | 29, 30, 31, 32 | syl2an3an 1419 |
. . . . . . 7
⊢
((((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) → ((2^{nd} ‘𝐴) = (2^{nd} ‘𝐵) ↔
((♯‘(1^{st} ‘𝐴)) = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈
(0...(♯‘(1^{st} ‘𝐴)))((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |
34 | 33 | adantr 484 |
. . . . . 6
⊢
(((((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) ∧ ((♯‘(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}
‘𝐵)‘𝑥)))) |
35 | 27, 34 | anbi12d 633 |
. . . . 5
⊢
(((((1^{st} ‘𝐴) ∈ Word dom (iEdg‘𝐺) ∧ (2^{nd}
‘𝐴):(0...(♯‘(1^{st}
‘𝐴)))⟶(Vtx‘𝐺)) ∧ ((1^{st} ‘𝐵) ∈ Word dom
(iEdg‘𝐺) ∧
(2^{nd} ‘𝐵):(0...(♯‘(1^{st}
‘𝐵)))⟶(Vtx‘𝐺))) ∧ ((♯‘(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}
‘𝐵)‘𝑥))))) |
36 | 9, 24, 35 | syl2anc 587 |
. . . 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}
‘𝐵)‘𝑥))))) |
37 | 36 | 3adant3 1129 |
. . 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} ‘𝐵)‘𝑥))))) |
38 | | eqeq1 2802 |
. . . . . . 7
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → (𝑁 = (♯‘(1^{st}
‘𝐵)) ↔
(♯‘(1^{st} ‘𝐴)) = (♯‘(1^{st}
‘𝐵)))) |
39 | | oveq2 7144 |
. . . . . . . 8
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → (0..^𝑁) = (0..^(♯‘(1^{st}
‘𝐴)))) |
40 | 39 | raleqdv 3364 |
. . . . . . 7
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → (∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ↔ ∀𝑥 ∈ (0..^(♯‘(1^{st}
‘𝐴)))((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥))) |
41 | 38, 40 | anbi12d 633 |
. . . . . 6
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → ((𝑁 = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥)) ↔ ((♯‘(1^{st}
‘𝐴)) =
(♯‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0..^(♯‘(1^{st}
‘𝐴)))((1^{st}
‘𝐴)‘𝑥) = ((1^{st}
‘𝐵)‘𝑥)))) |
42 | | oveq2 7144 |
. . . . . . . 8
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → (0...𝑁) = (0...(♯‘(1^{st}
‘𝐴)))) |
43 | 42 | raleqdv 3364 |
. . . . . . 7
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → (∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥) ↔ ∀𝑥 ∈ (0...(♯‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥))) |
44 | 38, 43 | anbi12d 633 |
. . . . . 6
⊢ (𝑁 =
(♯‘(1^{st} ‘𝐴)) → ((𝑁 = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)) ↔ ((♯‘(1^{st}
‘𝐴)) =
(♯‘(1^{st} ‘𝐵)) ∧ ∀𝑥 ∈ (0...(♯‘(1^{st}
‘𝐴)))((2^{nd}
‘𝐴)‘𝑥) = ((2^{nd}
‘𝐵)‘𝑥)))) |
45 | 41, 44 | anbi12d 633 |
. . . . 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} ‘𝐵)‘𝑥))))) |
46 | 45 | bibi2d 346 |
. . . 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}
‘𝐵)‘𝑥)))))) |
47 | 46 | 3ad2ant3 1132 |
. . 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}
‘𝐵)‘𝑥)))))) |
48 | 37, 47 | mpbird 260 |
. 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} ‘𝐵)‘𝑥))))) |
49 | | 1st2ndb 7714 |
. . . . 5
⊢ (𝐴 ∈ (V × V) ↔
𝐴 = ⟨(1^{st}
‘𝐴), (2^{nd}
‘𝐴)⟩) |
50 | 10, 49 | sylibr 237 |
. . . 4
⊢ (𝐴 ∈ (Walks‘𝐺) → 𝐴 ∈ (V × V)) |
51 | | 1st2ndb 7714 |
. . . . 5
⊢ (𝐵 ∈ (V × V) ↔
𝐵 = ⟨(1^{st}
‘𝐵), (2^{nd}
‘𝐵)⟩) |
52 | 17, 51 | sylibr 237 |
. . . 4
⊢ (𝐵 ∈ (Walks‘𝐺) → 𝐵 ∈ (V × V)) |
53 | | xpopth 7715 |
. . . 4
⊢ ((𝐴 ∈ (V × V) ∧
𝐵 ∈ (V × V))
→ (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd} ‘𝐴) = (2^{nd} ‘𝐵)) ↔ 𝐴 = 𝐵)) |
54 | 50, 52, 53 | syl2an 598 |
. . 3
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺)) → (((1^{st} ‘𝐴) = (1^{st} ‘𝐵) ∧ (2^{nd}
‘𝐴) = (2^{nd}
‘𝐵)) ↔ 𝐴 = 𝐵)) |
55 | 54 | 3adant3 1129 |
. 2
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1^{st}
‘𝐴))) →
(((1^{st} ‘𝐴)
= (1^{st} ‘𝐵)
∧ (2^{nd} ‘𝐴) = (2^{nd} ‘𝐵)) ↔ 𝐴 = 𝐵)) |
56 | | 3anass 1092 |
. . . 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} ‘𝐵)‘𝑥)))) |
57 | | anandi 675 |
. . . 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} ‘𝐵)‘𝑥)))) |
58 | 56, 57 | bitr2i 279 |
. . 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} ‘𝐵)‘𝑥))) |
59 | 58 | 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} ‘𝐵)‘𝑥)))) |
60 | 48, 55, 59 | 3bitr3d 312 |
1
⊢ ((𝐴 ∈ (Walks‘𝐺) ∧ 𝐵 ∈ (Walks‘𝐺) ∧ 𝑁 = (♯‘(1^{st}
‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (♯‘(1^{st}
‘𝐵)) ∧
∀𝑥 ∈ (0..^𝑁)((1^{st} ‘𝐴)‘𝑥) = ((1^{st} ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2^{nd} ‘𝐴)‘𝑥) = ((2^{nd} ‘𝐵)‘𝑥)))) |