Step | Hyp | Ref
| Expression |
1 | | uspgrupgr 40406 |
. . 3
⊢ (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph
) |
2 | | wlkwwlkbij.t |
. . . 4
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} |
3 | | wlkwwlkbij.w |
. . . 4
⊢ 𝑊 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃} |
4 | | wlkwwlkbij.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) |
5 | 2, 3, 4 | wlkwwlkfun 41092 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) |
6 | 1, 5 | syl3an1 1351 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) |
7 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑡 = 𝑣 → (2nd ‘𝑡) = (2nd ‘𝑣)) |
8 | | fvex 6113 |
. . . . . . 7
⊢
(2nd ‘𝑣) ∈ V |
9 | 7, 4, 8 | fvmpt 6191 |
. . . . . 6
⊢ (𝑣 ∈ 𝑇 → (𝐹‘𝑣) = (2nd ‘𝑣)) |
10 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑡 = 𝑤 → (2nd ‘𝑡) = (2nd ‘𝑤)) |
11 | | fvex 6113 |
. . . . . . 7
⊢
(2nd ‘𝑤) ∈ V |
12 | 10, 4, 11 | fvmpt 6191 |
. . . . . 6
⊢ (𝑤 ∈ 𝑇 → (𝐹‘𝑤) = (2nd ‘𝑤)) |
13 | 9, 12 | eqeqan12d 2626 |
. . . . 5
⊢ ((𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇) → ((𝐹‘𝑣) = (𝐹‘𝑤) ↔ (2nd ‘𝑣) = (2nd ‘𝑤))) |
14 | 13 | adantl 481 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇)) → ((𝐹‘𝑣) = (𝐹‘𝑤) ↔ (2nd ‘𝑣) = (2nd ‘𝑤))) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑣 → (1st ‘𝑝) = (1st ‘𝑣)) |
16 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑝 = 𝑣 → (#‘(1st ‘𝑝)) = (#‘(1st
‘𝑣))) |
17 | 16 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑝 = 𝑣 → ((#‘(1st
‘𝑝)) = 𝑁 ↔ (#‘(1st
‘𝑣)) = 𝑁)) |
18 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑣 → (2nd ‘𝑝) = (2nd ‘𝑣)) |
19 | 18 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑝 = 𝑣 → ((2nd ‘𝑝)‘0) = ((2nd
‘𝑣)‘0)) |
20 | 19 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑝 = 𝑣 → (((2nd ‘𝑝)‘0) = 𝑃 ↔ ((2nd ‘𝑣)‘0) = 𝑃)) |
21 | 17, 20 | anbi12d 743 |
. . . . . . 7
⊢ (𝑝 = 𝑣 → (((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃) ↔
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃))) |
22 | 21, 2 | elrab2 3333 |
. . . . . 6
⊢ (𝑣 ∈ 𝑇 ↔ (𝑣 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑣)) = 𝑁 ∧ ((2nd
‘𝑣)‘0) = 𝑃))) |
23 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (1st ‘𝑝) = (1st ‘𝑤)) |
24 | 23 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑝 = 𝑤 → (#‘(1st ‘𝑝)) = (#‘(1st
‘𝑤))) |
25 | 24 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑝 = 𝑤 → ((#‘(1st
‘𝑝)) = 𝑁 ↔ (#‘(1st
‘𝑤)) = 𝑁)) |
26 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑤 → (2nd ‘𝑝) = (2nd ‘𝑤)) |
27 | 26 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑝 = 𝑤 → ((2nd ‘𝑝)‘0) = ((2nd
‘𝑤)‘0)) |
28 | 27 | eqeq1d 2612 |
. . . . . . . 8
⊢ (𝑝 = 𝑤 → (((2nd ‘𝑝)‘0) = 𝑃 ↔ ((2nd ‘𝑤)‘0) = 𝑃)) |
29 | 25, 28 | anbi12d 743 |
. . . . . . 7
⊢ (𝑝 = 𝑤 → (((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃) ↔
((#‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃))) |
30 | 29, 2 | elrab2 3333 |
. . . . . 6
⊢ (𝑤 ∈ 𝑇 ↔ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃))) |
31 | 22, 30 | anbi12i 729 |
. . . . 5
⊢ ((𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇) ↔ ((𝑣 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑣)) = 𝑁 ∧ ((2nd
‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) |
32 | | 3simpb 1052 |
. . . . . . 7
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝐺 ∈ USPGraph ∧ 𝑁 ∈
ℕ0)) |
33 | 32 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) → (𝐺 ∈ USPGraph ∧ 𝑁 ∈
ℕ0)) |
34 | | simpl 472 |
. . . . . . . . 9
⊢
(((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃) → (#‘(1st
‘𝑣)) = 𝑁) |
35 | 34 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) → (𝑣 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑣)) = 𝑁)) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ (((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃))) → (𝑣 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑣)) = 𝑁)) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) → (𝑣 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑣)) = 𝑁)) |
38 | | simpl 472 |
. . . . . . . . 9
⊢
(((#‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃) → (#‘(1st
‘𝑤)) = 𝑁) |
39 | 38 | anim2i 591 |
. . . . . . . 8
⊢ ((𝑤 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑃)) → (𝑤 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑤)) = 𝑁)) |
40 | 39 | adantl 481 |
. . . . . . 7
⊢ (((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃))) → (𝑤 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑤)) = 𝑁)) |
41 | 40 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) → (𝑤 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑤)) = 𝑁)) |
42 | | uspgr2wlkeq2 40855 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
∧ (𝑣 ∈
(1Walks‘𝐺) ∧
(#‘(1st ‘𝑣)) = 𝑁) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ (#‘(1st
‘𝑤)) = 𝑁)) → ((2nd
‘𝑣) = (2nd
‘𝑤) → 𝑣 = 𝑤)) |
43 | 33, 37, 41, 42 | syl3anc 1318 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ ((𝑣 ∈ (1Walks‘𝐺) ∧
((#‘(1st ‘𝑣)) = 𝑁 ∧ ((2nd ‘𝑣)‘0) = 𝑃)) ∧ (𝑤 ∈ (1Walks‘𝐺) ∧ ((#‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑃)))) → ((2nd
‘𝑣) = (2nd
‘𝑤) → 𝑣 = 𝑤)) |
44 | 31, 43 | sylan2b 491 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇)) → ((2nd ‘𝑣) = (2nd ‘𝑤) → 𝑣 = 𝑤)) |
45 | 14, 44 | sylbid 229 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑣 ∈ 𝑇 ∧ 𝑤 ∈ 𝑇)) → ((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤)) |
46 | 45 | ralrimivva 2954 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∀𝑣 ∈ 𝑇 ∀𝑤 ∈ 𝑇 ((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤)) |
47 | | dff13 6416 |
. 2
⊢ (𝐹:𝑇–1-1→𝑊 ↔ (𝐹:𝑇⟶𝑊 ∧ ∀𝑣 ∈ 𝑇 ∀𝑤 ∈ 𝑇 ((𝐹‘𝑣) = (𝐹‘𝑤) → 𝑣 = 𝑤))) |
48 | 6, 46, 47 | sylanbrc 695 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊) |