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