Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . . . 6
⊢
(1st ‘𝑤) ∈ V |
2 | | breq1 4656 |
. . . . . 6
⊢ (𝑓 = (1st ‘𝑤) → (𝑓(Walks‘𝐺)(2nd ‘𝑤) ↔ (1st ‘𝑤)(Walks‘𝐺)(2nd ‘𝑤))) |
3 | 1, 2 | spcev 3300 |
. . . . 5
⊢
((1st ‘𝑤)(Walks‘𝐺)(2nd ‘𝑤) → ∃𝑓 𝑓(Walks‘𝐺)(2nd ‘𝑤)) |
4 | | wlkiswwlks 26762 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∃𝑓 𝑓(Walks‘𝐺)(2nd ‘𝑤) ↔ (2nd ‘𝑤) ∈ (WWalks‘𝐺))) |
5 | 3, 4 | syl5ib 234 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
((1st ‘𝑤)(Walks‘𝐺)(2nd ‘𝑤) → (2nd ‘𝑤) ∈ (WWalks‘𝐺))) |
6 | | wlkcpr 26524 |
. . . . 5
⊢ (𝑤 ∈ (Walks‘𝐺) ↔ (1st
‘𝑤)(Walks‘𝐺)(2nd ‘𝑤)) |
7 | 6 | biimpi 206 |
. . . 4
⊢ (𝑤 ∈ (Walks‘𝐺) → (1st
‘𝑤)(Walks‘𝐺)(2nd ‘𝑤)) |
8 | 5, 7 | impel 485 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (Walks‘𝐺)) → (2nd
‘𝑤) ∈
(WWalks‘𝐺)) |
9 | | wlkpwwlkf1ouspgr.f |
. . 3
⊢ 𝐹 = (𝑤 ∈ (Walks‘𝐺) ↦ (2nd ‘𝑤)) |
10 | 8, 9 | fmptd 6385 |
. 2
⊢ (𝐺 ∈ USPGraph → 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) |
11 | | simpr 477 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) |
12 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Walks‘𝐺) → 𝐹 = (𝑤 ∈ (Walks‘𝐺) ↦ (2nd ‘𝑤))) |
13 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (2nd ‘𝑤) = (2nd ‘𝑥)) |
14 | 13 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (Walks‘𝐺) ∧ 𝑤 = 𝑥) → (2nd ‘𝑤) = (2nd ‘𝑥)) |
15 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Walks‘𝐺) → 𝑥 ∈ (Walks‘𝐺)) |
16 | | fvexd 6203 |
. . . . . . . . 9
⊢ (𝑥 ∈ (Walks‘𝐺) → (2nd
‘𝑥) ∈
V) |
17 | 12, 14, 15, 16 | fvmptd 6288 |
. . . . . . . 8
⊢ (𝑥 ∈ (Walks‘𝐺) → (𝐹‘𝑥) = (2nd ‘𝑥)) |
18 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ (Walks‘𝐺) → 𝐹 = (𝑤 ∈ (Walks‘𝐺) ↦ (2nd ‘𝑤))) |
19 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (2nd ‘𝑤) = (2nd ‘𝑦)) |
20 | 19 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (Walks‘𝐺) ∧ 𝑤 = 𝑦) → (2nd ‘𝑤) = (2nd ‘𝑦)) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 ∈ (Walks‘𝐺) → 𝑦 ∈ (Walks‘𝐺)) |
22 | | fvexd 6203 |
. . . . . . . . 9
⊢ (𝑦 ∈ (Walks‘𝐺) → (2nd
‘𝑦) ∈
V) |
23 | 18, 20, 21, 22 | fvmptd 6288 |
. . . . . . . 8
⊢ (𝑦 ∈ (Walks‘𝐺) → (𝐹‘𝑦) = (2nd ‘𝑦)) |
24 | 17, 23 | eqeqan12d 2638 |
. . . . . . 7
⊢ ((𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ (𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺))) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
26 | | uspgr2wlkeqi 26544 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ (𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺)) ∧ (2nd ‘𝑥) = (2nd ‘𝑦)) → 𝑥 = 𝑦) |
27 | 26 | ad4ant134 1296 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ (𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺))) ∧ (2nd ‘𝑥) = (2nd ‘𝑦)) → 𝑥 = 𝑦) |
28 | 27 | ex 450 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ (𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺))) → ((2nd ‘𝑥) = (2nd ‘𝑦) → 𝑥 = 𝑦)) |
29 | 25, 28 | sylbid 230 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ (𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 ∈ (Walks‘𝐺))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
30 | 29 | ralrimivva 2971 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → ∀𝑥 ∈ (Walks‘𝐺)∀𝑦 ∈ (Walks‘𝐺)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
31 | | dff13 6512 |
. . . 4
⊢ (𝐹:(Walks‘𝐺)–1-1→(WWalks‘𝐺) ↔ (𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺) ∧ ∀𝑥 ∈ (Walks‘𝐺)∀𝑦 ∈ (Walks‘𝐺)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
32 | 11, 30, 31 | sylanbrc 698 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → 𝐹:(Walks‘𝐺)–1-1→(WWalks‘𝐺)) |
33 | | wlkiswwlks 26762 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph →
(∃𝑓 𝑓(Walks‘𝐺)𝑦 ↔ 𝑦 ∈ (WWalks‘𝐺))) |
34 | 33 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → (∃𝑓 𝑓(Walks‘𝐺)𝑦 ↔ 𝑦 ∈ (WWalks‘𝐺))) |
35 | | df-br 4654 |
. . . . . . . . . . 11
⊢ (𝑓(Walks‘𝐺)𝑦 ↔ 〈𝑓, 𝑦〉 ∈ (Walks‘𝐺)) |
36 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
37 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
38 | 36, 37 | op2nd 7177 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈𝑓, 𝑦〉) = 𝑦 |
39 | 38 | eqcomi 2631 |
. . . . . . . . . . . 12
⊢ 𝑦 = (2nd
‘〈𝑓, 𝑦〉) |
40 | | opex 4932 |
. . . . . . . . . . . . 13
⊢
〈𝑓, 𝑦〉 ∈ V |
41 | | eleq1 2689 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (𝑥 ∈ (Walks‘𝐺) ↔ 〈𝑓, 𝑦〉 ∈ (Walks‘𝐺))) |
42 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (2nd ‘𝑥) = (2nd
‘〈𝑓, 𝑦〉)) |
43 | 42 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (𝑦 = (2nd ‘𝑥) ↔ 𝑦 = (2nd ‘〈𝑓, 𝑦〉))) |
44 | 41, 43 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑓, 𝑦〉 → ((𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥)) ↔ (〈𝑓, 𝑦〉 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘〈𝑓, 𝑦〉)))) |
45 | 40, 44 | spcev 3300 |
. . . . . . . . . . . 12
⊢
((〈𝑓, 𝑦〉 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘〈𝑓, 𝑦〉)) → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
46 | 39, 45 | mpan2 707 |
. . . . . . . . . . 11
⊢
(〈𝑓, 𝑦〉 ∈ (Walks‘𝐺) → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
47 | 35, 46 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑓(Walks‘𝐺)𝑦 → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
48 | 47 | exlimiv 1858 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓(Walks‘𝐺)𝑦 → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
49 | 34, 48 | syl6bir 244 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → (𝑦 ∈ (WWalks‘𝐺) → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥)))) |
50 | 49 | imp 445 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ 𝑦 ∈ (WWalks‘𝐺)) → ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
51 | | df-rex 2918 |
. . . . . . 7
⊢
(∃𝑥 ∈
(Walks‘𝐺)𝑦 = (2nd ‘𝑥) ↔ ∃𝑥(𝑥 ∈ (Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
52 | 50, 51 | sylibr 224 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ 𝑦 ∈ (WWalks‘𝐺)) → ∃𝑥 ∈ (Walks‘𝐺)𝑦 = (2nd ‘𝑥)) |
53 | 17 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑥 ∈ (Walks‘𝐺) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = (2nd ‘𝑥))) |
54 | 53 | rexbiia 3040 |
. . . . . 6
⊢
(∃𝑥 ∈
(Walks‘𝐺)𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ (Walks‘𝐺)𝑦 = (2nd ‘𝑥)) |
55 | 52, 54 | sylibr 224 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) ∧ 𝑦 ∈ (WWalks‘𝐺)) → ∃𝑥 ∈ (Walks‘𝐺)𝑦 = (𝐹‘𝑥)) |
56 | 55 | ralrimiva 2966 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → ∀𝑦 ∈ (WWalks‘𝐺)∃𝑥 ∈ (Walks‘𝐺)𝑦 = (𝐹‘𝑥)) |
57 | | dffo3 6374 |
. . . 4
⊢ (𝐹:(Walks‘𝐺)–onto→(WWalks‘𝐺) ↔ (𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺) ∧ ∀𝑦 ∈ (WWalks‘𝐺)∃𝑥 ∈ (Walks‘𝐺)𝑦 = (𝐹‘𝑥))) |
58 | 11, 56, 57 | sylanbrc 698 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → 𝐹:(Walks‘𝐺)–onto→(WWalks‘𝐺)) |
59 | | df-f1o 5895 |
. . 3
⊢ (𝐹:(Walks‘𝐺)–1-1-onto→(WWalks‘𝐺) ↔ (𝐹:(Walks‘𝐺)–1-1→(WWalks‘𝐺) ∧ 𝐹:(Walks‘𝐺)–onto→(WWalks‘𝐺))) |
60 | 32, 58, 59 | sylanbrc 698 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(Walks‘𝐺)⟶(WWalks‘𝐺)) → 𝐹:(Walks‘𝐺)–1-1-onto→(WWalks‘𝐺)) |
61 | 10, 60 | mpdan 702 |
1
⊢ (𝐺 ∈ USPGraph → 𝐹:(Walks‘𝐺)–1-1-onto→(WWalks‘𝐺)) |