Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . . 5
⊢
(Walks‘𝐺)
∈ V |
2 | 1 | mptrabex 6488 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ∈
V |
3 | 2 | resex 5443 |
. . 3
⊢ ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}) ∈ V |
4 | | eqid 2622 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) = (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) |
5 | | usgruspgr 26073 |
. . . . . 6
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph
) |
6 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑡 → (1st ‘𝑞) = (1st ‘𝑡)) |
7 | 6 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑞 = 𝑡 → (#‘(1st ‘𝑞)) = (#‘(1st
‘𝑡))) |
8 | 7 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑞 = 𝑡 → ((#‘(1st
‘𝑞)) = 𝑁 ↔ (#‘(1st
‘𝑡)) = 𝑁)) |
9 | 8 | cbvrabv 3199 |
. . . . . . 7
⊢ {𝑞 ∈ (Walks‘𝐺) ∣
(#‘(1st ‘𝑞)) = 𝑁} = {𝑡 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑡)) = 𝑁} |
10 | | eqid 2622 |
. . . . . . 7
⊢ (𝑁 WWalksN 𝐺) = (𝑁 WWalksN 𝐺) |
11 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑝 = 𝑠 → (2nd ‘𝑝) = (2nd ‘𝑠)) |
12 | 11 | cbvmptv 4750 |
. . . . . . 7
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) = (𝑠 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑠)) |
13 | 9, 10, 12 | wlknwwlksnbij 26777 |
. . . . . 6
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(#‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)):{𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁}–1-1-onto→(𝑁 WWalksN 𝐺)) |
14 | 5, 13 | sylan 488 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(#‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)):{𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁}–1-1-onto→(𝑁 WWalksN 𝐺)) |
15 | 14 | 3adant3 1081 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
(𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(#‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)):{𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁}–1-1-onto→(𝑁 WWalksN 𝐺)) |
16 | | fveq1 6190 |
. . . . . 6
⊢ (𝑤 = (2nd ‘𝑝) → (𝑤‘0) = ((2nd ‘𝑝)‘0)) |
17 | 16 | eqeq1d 2624 |
. . . . 5
⊢ (𝑤 = (2nd ‘𝑝) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
18 | 17 | 3ad2ant3 1084 |
. . . 4
⊢ (((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) ∧ 𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ 𝑤 = (2nd ‘𝑝)) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
19 | 4, 15, 18 | f1oresrab 6395 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(#‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}):{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
20 | | f1oeq1 6127 |
. . . 4
⊢ (𝑓 = ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}) → (𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}):{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
21 | 20 | spcegv 3294 |
. . 3
⊢ (((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}) ∈ V → (((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}):{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} → ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
22 | 3, 19, 21 | mpsyl 68 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
23 | | df-rab 2921 |
. . . . 5
⊢ {𝑝 ∈ (Walks‘𝐺) ∣
((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)} = {𝑝 ∣ (𝑝 ∈ (Walks‘𝐺) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))} |
24 | | anass 681 |
. . . . . . 7
⊢ (((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ (𝑝 ∈ (Walks‘𝐺) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))) |
25 | 24 | bicomi 214 |
. . . . . 6
⊢ ((𝑝 ∈ (Walks‘𝐺) ∧
((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)) ↔ ((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
26 | 25 | abbii 2739 |
. . . . 5
⊢ {𝑝 ∣ (𝑝 ∈ (Walks‘𝐺) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))} = {𝑝 ∣ ((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
27 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (1st ‘𝑞) = (1st ‘𝑝)) |
28 | 27 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → (#‘(1st ‘𝑞)) = (#‘(1st
‘𝑝))) |
29 | 28 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑝 → ((#‘(1st
‘𝑞)) = 𝑁 ↔ (#‘(1st
‘𝑝)) = 𝑁)) |
30 | 29 | elrab 3363 |
. . . . . . . . 9
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↔ (𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁)) |
31 | 30 | anbi1i 731 |
. . . . . . . 8
⊢ ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ ((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
32 | 31 | bicomi 214 |
. . . . . . 7
⊢ (((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
33 | 32 | abbii 2739 |
. . . . . 6
⊢ {𝑝 ∣ ((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∣ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
34 | | df-rab 2921 |
. . . . . 6
⊢ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} = {𝑝 ∣ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
35 | 33, 34 | eqtr4i 2647 |
. . . . 5
⊢ {𝑝 ∣ ((𝑝 ∈ (Walks‘𝐺) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} |
36 | 23, 26, 35 | 3eqtri 2648 |
. . . 4
⊢ {𝑝 ∈ (Walks‘𝐺) ∣
((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} |
37 | | f1oeq2 6128 |
. . . 4
⊢ ({𝑝 ∈ (Walks‘𝐺) ∣
((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} → (𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
38 | 36, 37 | mp1i 13 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
(𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
39 | 38 | exbidv 1850 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
(∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
40 | 22, 39 | mpbird 247 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈
(Vtx‘𝐺)) →
∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |