Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . 5
⊢ (𝑉 Walks 𝐸) ∈ V |
2 | 1 | mptrabex 6392 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ∈
V |
3 | 2 | resex 5363 |
. . 3
⊢ ((𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}) ∈ V |
4 | | eqid 2610 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) = (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) |
5 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑞 = 𝑡 → (1st ‘𝑞) = (1st ‘𝑡)) |
6 | 5 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑞 = 𝑡 → (#‘(1st ‘𝑞)) = (#‘(1st
‘𝑡))) |
7 | 6 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑞 = 𝑡 → ((#‘(1st
‘𝑞)) = 𝑁 ↔ (#‘(1st
‘𝑡)) = 𝑁)) |
8 | 7 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} = {𝑡 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑡)) = 𝑁} |
9 | | eqid 2610 |
. . . . . 6
⊢ ((𝑉 WWalksN 𝐸)‘𝑁) = ((𝑉 WWalksN 𝐸)‘𝑁) |
10 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑝 = 𝑠 → (2nd ‘𝑝) = (2nd ‘𝑠)) |
11 | 10 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) = (𝑠 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑠)) |
12 | 8, 9, 11 | wlknwwlknbij 26241 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0) → (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)):{𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁}–1-1-onto→((𝑉 WWalksN 𝐸)‘𝑁)) |
13 | 12 | 3adant3 1074 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)):{𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁}–1-1-onto→((𝑉 WWalksN 𝐸)‘𝑁)) |
14 | | fveq1 6102 |
. . . . . 6
⊢ (𝑤 = (2nd ‘𝑝) → (𝑤‘0) = ((2nd ‘𝑝)‘0)) |
15 | 14 | eqeq1d 2612 |
. . . . 5
⊢ (𝑤 = (2nd ‘𝑝) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
16 | 15 | 3ad2ant3 1077 |
. . . 4
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) ∧ 𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ 𝑤 = (2nd ‘𝑝)) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
17 | 4, 13, 16 | f1oresrab 6302 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → ((𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}):{𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
18 | | f1oeq1 6040 |
. . . 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) = 𝑋})) |
19 | 18 | spcegv 3267 |
. . 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) = 𝑋})) |
20 | 3, 17, 19 | mpsyl 66 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |
21 | | df-rab 2905 |
. . . . 5
⊢ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∣ (𝑝 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))} |
22 | | anass 679 |
. . . . . . 7
⊢ (((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ (𝑝 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))) |
23 | 22 | bicomi 213 |
. . . . . 6
⊢ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)) ↔ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
24 | 23 | abbii 2726 |
. . . . 5
⊢ {𝑝 ∣ (𝑝 ∈ (𝑉 Walks 𝐸) ∧ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋))} = {𝑝 ∣ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
25 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → (1st ‘𝑞) = (1st ‘𝑝)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → (#‘(1st ‘𝑞)) = (#‘(1st
‘𝑝))) |
27 | 26 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑝 → ((#‘(1st
‘𝑞)) = 𝑁 ↔ (#‘(1st
‘𝑝)) = 𝑁)) |
28 | 27 | elrab 3331 |
. . . . . . . . 9
⊢ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ↔ (𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁)) |
29 | 28 | anbi1i 727 |
. . . . . . . 8
⊢ ((𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
30 | 29 | bicomi 213 |
. . . . . . 7
⊢ (((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋) ↔ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)) |
31 | 30 | abbii 2726 |
. . . . . 6
⊢ {𝑝 ∣ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∣ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
32 | | df-rab 2905 |
. . . . . 6
⊢ {𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} = {𝑝 ∣ (𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
33 | 31, 32 | eqtr4i 2635 |
. . . . 5
⊢ {𝑝 ∣ ((𝑝 ∈ (𝑉 Walks 𝐸) ∧ (#‘(1st
‘𝑝)) = 𝑁) ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} |
34 | 21, 24, 33 | 3eqtri 2636 |
. . . 4
⊢ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} |
35 | | f1oeq2 6041 |
. . . 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) = 𝑋})) |
36 | 34, 35 | mp1i 13 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ↔ 𝑓:{𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋})) |
37 | 36 | exbidv 1837 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋} ↔ ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (𝑉 Walks 𝐸) ∣ (#‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋})) |
38 | 20, 37 | mpbird 246 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑋}) |