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