Step | Hyp | Ref
| Expression |
1 | | wlknwwlknbij.t |
. . . 4
⊢ 𝑇 = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} |
2 | | wlknwwlknbij.w |
. . . 4
⊢ 𝑊 = ((𝑉 WWalksN 𝐸)‘𝑁) |
3 | | wlknwwlknbij.f |
. . . 4
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) |
4 | 1, 2, 3 | wlknwwlknfun 26238 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝐹:𝑇⟶𝑊) |
5 | 4 | adantl 481 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) |
6 | 2 | eleq2i 2680 |
. . . . 5
⊢ (𝑝 ∈ 𝑊 ↔ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) |
7 | | wlklniswwlkn 26229 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → (∃𝑓(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 𝑁) ↔ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁))) |
8 | | df-br 4584 |
. . . . . . . . . . . . 13
⊢ (𝑓(𝑉 Walks 𝐸)𝑝 ↔ 〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸)) |
9 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
10 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑝 ∈ V |
11 | 9, 10 | op1st 7067 |
. . . . . . . . . . . . . . . 16
⊢
(1st ‘〈𝑓, 𝑝〉) = 𝑓 |
12 | 11 | eqcomi 2619 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 = (1st
‘〈𝑓, 𝑝〉) |
13 | 12 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢
(#‘𝑓) =
(#‘(1st ‘〈𝑓, 𝑝〉)) |
14 | 13 | eqeq1i 2615 |
. . . . . . . . . . . . 13
⊢
((#‘𝑓) = 𝑁 ↔ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) |
15 | | elex 3185 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) → 〈𝑓, 𝑝〉 ∈ V) |
16 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 〈𝑓, 𝑝〉 → (𝑢 ∈ (𝑉 Walks 𝐸) ↔ 〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸))) |
17 | 16 | biimparc 503 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) → 𝑢 ∈ (𝑉 Walks 𝐸)) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) ∧ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) → 𝑢 ∈ (𝑉 Walks 𝐸)) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 〈𝑓, 𝑝〉 → (1st ‘𝑢) = (1st
‘〈𝑓, 𝑝〉)) |
20 | 19 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 〈𝑓, 𝑝〉 → (#‘(1st
‘𝑢)) =
(#‘(1st ‘〈𝑓, 𝑝〉))) |
21 | 20 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 〈𝑓, 𝑝〉 → ((#‘(1st
‘𝑢)) = 𝑁 ↔ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁)) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) → ((#‘(1st
‘𝑢)) = 𝑁 ↔ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁)) |
23 | 22 | biimpar 501 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) ∧ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) → (#‘(1st
‘𝑢)) = 𝑁) |
24 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 〈𝑓, 𝑝〉 → (2nd ‘𝑢) = (2nd
‘〈𝑓, 𝑝〉)) |
25 | 9, 10 | op2nd 7068 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(2nd ‘〈𝑓, 𝑝〉) = 𝑝 |
26 | 24, 25 | syl6req 2661 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 〈𝑓, 𝑝〉 → 𝑝 = (2nd ‘𝑢)) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) → 𝑝 = (2nd ‘𝑢)) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) ∧ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) → 𝑝 = (2nd ‘𝑢)) |
29 | 18, 23, 28 | jca31 555 |
. . . . . . . . . . . . . . . 16
⊢
(((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) ∧ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) → ((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
30 | 29 | ex 449 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ 𝑢 = 〈𝑓, 𝑝〉) → ((#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁 → ((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢)))) |
31 | 15, 30 | spcimedv 3265 |
. . . . . . . . . . . . . 14
⊢
(〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) → ((#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁 → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢)))) |
32 | 31 | imp 444 |
. . . . . . . . . . . . 13
⊢
((〈𝑓, 𝑝〉 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘〈𝑓, 𝑝〉)) = 𝑁) → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
33 | 8, 14, 32 | syl2anb 495 |
. . . . . . . . . . . 12
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 𝑁) → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
34 | 33 | exlimiv 1845 |
. . . . . . . . . . 11
⊢
(∃𝑓(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 𝑁) → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
35 | 7, 34 | syl6bir 243 |
. . . . . . . . . 10
⊢ (𝑉 USGrph 𝐸 → (𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢)))) |
36 | 35 | imp 444 |
. . . . . . . . 9
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
37 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 𝑢 → (1st ‘𝑝) = (1st ‘𝑢)) |
38 | 37 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 𝑢 → (#‘(1st ‘𝑝)) = (#‘(1st
‘𝑢))) |
39 | 38 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑢 → ((#‘(1st
‘𝑝)) = 𝑁 ↔ (#‘(1st
‘𝑢)) = 𝑁)) |
40 | 39 | elrab 3331 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} ↔ (𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁)) |
41 | 40 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} ∧ 𝑝 = (2nd ‘𝑢)) ↔ ((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
42 | 41 | exbii 1764 |
. . . . . . . . 9
⊢
(∃𝑢(𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} ∧ 𝑝 = (2nd ‘𝑢)) ↔ ∃𝑢((𝑢 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑢)) = 𝑁) ∧ 𝑝 = (2nd ‘𝑢))) |
43 | 36, 42 | sylibr 223 |
. . . . . . . 8
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ∃𝑢(𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} ∧ 𝑝 = (2nd ‘𝑢))) |
44 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑢 ∈
{𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁}𝑝 = (2nd ‘𝑢) ↔ ∃𝑢(𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁} ∧ 𝑝 = (2nd ‘𝑢))) |
45 | 43, 44 | sylibr 223 |
. . . . . . 7
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ∃𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁}𝑝 = (2nd ‘𝑢)) |
46 | 1 | rexeqi 3120 |
. . . . . . 7
⊢
(∃𝑢 ∈
𝑇 𝑝 = (2nd ‘𝑢) ↔ ∃𝑢 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑝)) = 𝑁}𝑝 = (2nd ‘𝑢)) |
47 | 45, 46 | sylibr 223 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ∃𝑢 ∈ 𝑇 𝑝 = (2nd ‘𝑢)) |
48 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑡 = 𝑢 → (2nd ‘𝑡) = (2nd ‘𝑢)) |
49 | | fvex 6113 |
. . . . . . . . 9
⊢
(2nd ‘𝑢) ∈ V |
50 | 48, 3, 49 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝑇 → (𝐹‘𝑢) = (2nd ‘𝑢)) |
51 | 50 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑢 ∈ 𝑇 → (𝑝 = (𝐹‘𝑢) ↔ 𝑝 = (2nd ‘𝑢))) |
52 | 51 | rexbiia 3022 |
. . . . . 6
⊢
(∃𝑢 ∈
𝑇 𝑝 = (𝐹‘𝑢) ↔ ∃𝑢 ∈ 𝑇 𝑝 = (2nd ‘𝑢)) |
53 | 47, 52 | sylibr 223 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ ((𝑉 WWalksN 𝐸)‘𝑁)) → ∃𝑢 ∈ 𝑇 𝑝 = (𝐹‘𝑢)) |
54 | 6, 53 | sylan2b 491 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑝 ∈ 𝑊) → ∃𝑢 ∈ 𝑇 𝑝 = (𝐹‘𝑢)) |
55 | 54 | ralrimiva 2949 |
. . 3
⊢ (𝑉 USGrph 𝐸 → ∀𝑝 ∈ 𝑊 ∃𝑢 ∈ 𝑇 𝑝 = (𝐹‘𝑢)) |
56 | 55 | adantr 480 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) →
∀𝑝 ∈ 𝑊 ∃𝑢 ∈ 𝑇 𝑝 = (𝐹‘𝑢)) |
57 | | dffo3 6282 |
. 2
⊢ (𝐹:𝑇–onto→𝑊 ↔ (𝐹:𝑇⟶𝑊 ∧ ∀𝑝 ∈ 𝑊 ∃𝑢 ∈ 𝑇 𝑝 = (𝐹‘𝑢))) |
58 | 5, 56, 57 | sylanbrc 695 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊) |