Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . 6
⊢
(1st ‘𝑤) ∈ V |
2 | | breq1 4586 |
. . . . . 6
⊢ (𝑓 = (1st ‘𝑤) → (𝑓(1Walks‘𝐺)(2nd ‘𝑤) ↔ (1st ‘𝑤)(1Walks‘𝐺)(2nd ‘𝑤))) |
3 | 1, 2 | spcev 3273 |
. . . . 5
⊢
((1st ‘𝑤)(1Walks‘𝐺)(2nd ‘𝑤) → ∃𝑓 𝑓(1Walks‘𝐺)(2nd ‘𝑤)) |
4 | | 1wlkiswwlks 41073 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∃𝑓 𝑓(1Walks‘𝐺)(2nd ‘𝑤) ↔ (2nd ‘𝑤) ∈ (WWalkS‘𝐺))) |
5 | 3, 4 | syl5ib 233 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
((1st ‘𝑤)(1Walks‘𝐺)(2nd ‘𝑤) → (2nd ‘𝑤) ∈ (WWalkS‘𝐺))) |
6 | | 1wlkcpr 40833 |
. . . . 5
⊢ (𝑤 ∈ (1Walks‘𝐺) ↔ (1st
‘𝑤)(1Walks‘𝐺)(2nd ‘𝑤)) |
7 | 6 | biimpi 205 |
. . . 4
⊢ (𝑤 ∈ (1Walks‘𝐺) → (1st
‘𝑤)(1Walks‘𝐺)(2nd ‘𝑤)) |
8 | 5, 7 | impel 484 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑤 ∈ (1Walks‘𝐺)) → (2nd
‘𝑤) ∈
(WWalkS‘𝐺)) |
9 | | 1wlkpwwlkf1ouspgr.f |
. . 3
⊢ 𝐹 = (𝑤 ∈ (1Walks‘𝐺) ↦ (2nd ‘𝑤)) |
10 | 8, 9 | fmptd 6292 |
. 2
⊢ (𝐺 ∈ USPGraph → 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) |
11 | | simpr 476 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) |
12 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1Walks‘𝐺) → 𝐹 = (𝑤 ∈ (1Walks‘𝐺) ↦ (2nd ‘𝑤))) |
13 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (2nd ‘𝑤) = (2nd ‘𝑥)) |
14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (1Walks‘𝐺) ∧ 𝑤 = 𝑥) → (2nd ‘𝑤) = (2nd ‘𝑥)) |
15 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1Walks‘𝐺) → 𝑥 ∈ (1Walks‘𝐺)) |
16 | | fvex 6113 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1Walks‘𝐺) → (2nd
‘𝑥) ∈
V) |
18 | 12, 14, 15, 17 | fvmptd 6197 |
. . . . . . . 8
⊢ (𝑥 ∈ (1Walks‘𝐺) → (𝐹‘𝑥) = (2nd ‘𝑥)) |
19 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1Walks‘𝐺) → 𝐹 = (𝑤 ∈ (1Walks‘𝐺) ↦ (2nd ‘𝑤))) |
20 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (2nd ‘𝑤) = (2nd ‘𝑦)) |
21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (1Walks‘𝐺) ∧ 𝑤 = 𝑦) → (2nd ‘𝑤) = (2nd ‘𝑦)) |
22 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1Walks‘𝐺) → 𝑦 ∈ (1Walks‘𝐺)) |
23 | | fvex 6113 |
. . . . . . . . . 10
⊢
(2nd ‘𝑦) ∈ V |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ (1Walks‘𝐺) → (2nd
‘𝑦) ∈
V) |
25 | 19, 21, 22, 24 | fvmptd 6197 |
. . . . . . . 8
⊢ (𝑦 ∈ (1Walks‘𝐺) → (𝐹‘𝑦) = (2nd ‘𝑦)) |
26 | 18, 25 | eqeqan12d 2626 |
. . . . . . 7
⊢ ((𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
27 | 26 | adantl 481 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ (𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺))) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (2nd ‘𝑥) = (2nd ‘𝑦))) |
28 | | uspgr2wlkeqi 40856 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ (𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝑥) = (2nd ‘𝑦)) → 𝑥 = 𝑦) |
29 | 28 | ad4ant134 1288 |
. . . . . . 7
⊢ ((((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ (𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺))) ∧ (2nd ‘𝑥) = (2nd ‘𝑦)) → 𝑥 = 𝑦) |
30 | 29 | ex 449 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ (𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺))) → ((2nd ‘𝑥) = (2nd ‘𝑦) → 𝑥 = 𝑦)) |
31 | 27, 30 | sylbid 229 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ (𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 ∈ (1Walks‘𝐺))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
32 | 31 | ralrimivva 2954 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → ∀𝑥 ∈ (1Walks‘𝐺)∀𝑦 ∈ (1Walks‘𝐺)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
33 | | dff13 6416 |
. . . 4
⊢ (𝐹:(1Walks‘𝐺)–1-1→(WWalkS‘𝐺) ↔ (𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺) ∧ ∀𝑥 ∈ (1Walks‘𝐺)∀𝑦 ∈ (1Walks‘𝐺)((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
34 | 11, 32, 33 | sylanbrc 695 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → 𝐹:(1Walks‘𝐺)–1-1→(WWalkS‘𝐺)) |
35 | | 1wlkiswwlks 41073 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USPGraph →
(∃𝑓 𝑓(1Walks‘𝐺)𝑦 ↔ 𝑦 ∈ (WWalkS‘𝐺))) |
36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → (∃𝑓 𝑓(1Walks‘𝐺)𝑦 ↔ 𝑦 ∈ (WWalkS‘𝐺))) |
37 | | df-br 4584 |
. . . . . . . . . . 11
⊢ (𝑓(1Walks‘𝐺)𝑦 ↔ 〈𝑓, 𝑦〉 ∈ (1Walks‘𝐺)) |
38 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
39 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
40 | 38, 39 | op2nd 7068 |
. . . . . . . . . . . . 13
⊢
(2nd ‘〈𝑓, 𝑦〉) = 𝑦 |
41 | 40 | eqcomi 2619 |
. . . . . . . . . . . 12
⊢ 𝑦 = (2nd
‘〈𝑓, 𝑦〉) |
42 | | opex 4859 |
. . . . . . . . . . . . 13
⊢
〈𝑓, 𝑦〉 ∈ V |
43 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (𝑥 ∈ (1Walks‘𝐺) ↔ 〈𝑓, 𝑦〉 ∈ (1Walks‘𝐺))) |
44 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (2nd ‘𝑥) = (2nd
‘〈𝑓, 𝑦〉)) |
45 | 44 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑓, 𝑦〉 → (𝑦 = (2nd ‘𝑥) ↔ 𝑦 = (2nd ‘〈𝑓, 𝑦〉))) |
46 | 43, 45 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑓, 𝑦〉 → ((𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥)) ↔ (〈𝑓, 𝑦〉 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘〈𝑓, 𝑦〉)))) |
47 | 42, 46 | spcev 3273 |
. . . . . . . . . . . 12
⊢
((〈𝑓, 𝑦〉 ∈
(1Walks‘𝐺) ∧
𝑦 = (2nd
‘〈𝑓, 𝑦〉)) → ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
48 | 41, 47 | mpan2 703 |
. . . . . . . . . . 11
⊢
(〈𝑓, 𝑦〉 ∈
(1Walks‘𝐺) →
∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
49 | 37, 48 | sylbi 206 |
. . . . . . . . . 10
⊢ (𝑓(1Walks‘𝐺)𝑦 → ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
50 | 49 | exlimiv 1845 |
. . . . . . . . 9
⊢
(∃𝑓 𝑓(1Walks‘𝐺)𝑦 → ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
51 | 36, 50 | syl6bir 243 |
. . . . . . . 8
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → (𝑦 ∈ (WWalkS‘𝐺) → ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥)))) |
52 | 51 | imp 444 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ 𝑦 ∈ (WWalkS‘𝐺)) → ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
53 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑥 ∈
(1Walks‘𝐺)𝑦 = (2nd ‘𝑥) ↔ ∃𝑥(𝑥 ∈ (1Walks‘𝐺) ∧ 𝑦 = (2nd ‘𝑥))) |
54 | 52, 53 | sylibr 223 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ 𝑦 ∈ (WWalkS‘𝐺)) → ∃𝑥 ∈ (1Walks‘𝐺)𝑦 = (2nd ‘𝑥)) |
55 | 18 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑥 ∈ (1Walks‘𝐺) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = (2nd ‘𝑥))) |
56 | 55 | rexbiia 3022 |
. . . . . 6
⊢
(∃𝑥 ∈
(1Walks‘𝐺)𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ (1Walks‘𝐺)𝑦 = (2nd ‘𝑥)) |
57 | 54, 56 | sylibr 223 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) ∧ 𝑦 ∈ (WWalkS‘𝐺)) → ∃𝑥 ∈ (1Walks‘𝐺)𝑦 = (𝐹‘𝑥)) |
58 | 57 | ralrimiva 2949 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → ∀𝑦 ∈ (WWalkS‘𝐺)∃𝑥 ∈ (1Walks‘𝐺)𝑦 = (𝐹‘𝑥)) |
59 | | dffo3 6282 |
. . . 4
⊢ (𝐹:(1Walks‘𝐺)–onto→(WWalkS‘𝐺) ↔ (𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺) ∧ ∀𝑦 ∈ (WWalkS‘𝐺)∃𝑥 ∈ (1Walks‘𝐺)𝑦 = (𝐹‘𝑥))) |
60 | 11, 58, 59 | sylanbrc 695 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → 𝐹:(1Walks‘𝐺)–onto→(WWalkS‘𝐺)) |
61 | | df-f1o 5811 |
. . 3
⊢ (𝐹:(1Walks‘𝐺)–1-1-onto→(WWalkS‘𝐺) ↔ (𝐹:(1Walks‘𝐺)–1-1→(WWalkS‘𝐺) ∧ 𝐹:(1Walks‘𝐺)–onto→(WWalkS‘𝐺))) |
62 | 34, 60, 61 | sylanbrc 695 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹:(1Walks‘𝐺)⟶(WWalkS‘𝐺)) → 𝐹:(1Walks‘𝐺)–1-1-onto→(WWalkS‘𝐺)) |
63 | 10, 62 | mpdan 699 |
1
⊢ (𝐺 ∈ USPGraph → 𝐹:(1Walks‘𝐺)–1-1-onto→(WWalkS‘𝐺)) |