Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . 3
⊢ (𝑉 Walks 𝐸) ∈ V |
2 | 1 | mptrabex 6392 |
. 2
⊢ (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) ∈
V |
3 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑝 = 𝑢 → (1st ‘𝑝) = (1st ‘𝑢)) |
4 | 3 | fveq2d 6107 |
. . . . . 6
⊢ (𝑝 = 𝑢 → (#‘(1st ‘𝑝)) = (#‘(1st
‘𝑢))) |
5 | 4 | eqeq1d 2612 |
. . . . 5
⊢ (𝑝 = 𝑢 → ((#‘(1st
‘𝑝)) = 𝑁 ↔ (#‘(1st
‘𝑢)) = 𝑁)) |
6 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑝 = 𝑢 → (2nd ‘𝑝) = (2nd ‘𝑢)) |
7 | 6 | fveq1d 6105 |
. . . . . 6
⊢ (𝑝 = 𝑢 → ((2nd ‘𝑝)‘0) = ((2nd
‘𝑢)‘0)) |
8 | 7 | eqeq1d 2612 |
. . . . 5
⊢ (𝑝 = 𝑢 → (((2nd ‘𝑝)‘0) = 𝑃 ↔ ((2nd ‘𝑢)‘0) = 𝑃)) |
9 | 5, 8 | anbi12d 743 |
. . . 4
⊢ (𝑝 = 𝑢 → (((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃) ↔
((#‘(1st ‘𝑢)) = 𝑁 ∧ ((2nd ‘𝑢)‘0) = 𝑃))) |
10 | 9 | cbvrabv 3172 |
. . 3
⊢ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} = {𝑢 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑢)) = 𝑁 ∧ ((2nd
‘𝑢)‘0) = 𝑃)} |
11 | | fveq1 6102 |
. . . . 5
⊢ (𝑤 = 𝑠 → (𝑤‘0) = (𝑠‘0)) |
12 | 11 | eqeq1d 2612 |
. . . 4
⊢ (𝑤 = 𝑠 → ((𝑤‘0) = 𝑃 ↔ (𝑠‘0) = 𝑃)) |
13 | 12 | cbvrabv 3172 |
. . 3
⊢ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} = {𝑠 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑠‘0) = 𝑃} |
14 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑝 → (1st ‘𝑡) = (1st ‘𝑝)) |
15 | 14 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑡 = 𝑝 → (#‘(1st ‘𝑡)) = (#‘(1st
‘𝑝))) |
16 | 15 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑡 = 𝑝 → ((#‘(1st
‘𝑡)) = 𝑁 ↔ (#‘(1st
‘𝑝)) = 𝑁)) |
17 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑡 = 𝑝 → (2nd ‘𝑡) = (2nd ‘𝑝)) |
18 | 17 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑡 = 𝑝 → ((2nd ‘𝑡)‘0) = ((2nd
‘𝑝)‘0)) |
19 | 18 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑡 = 𝑝 → (((2nd ‘𝑡)‘0) = 𝑃 ↔ ((2nd ‘𝑝)‘0) = 𝑃)) |
20 | 16, 19 | anbi12d 743 |
. . . . 5
⊢ (𝑡 = 𝑝 → (((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃) ↔
((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃))) |
21 | 20 | cbvrabv 3172 |
. . . 4
⊢ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} |
22 | | mpteq1 4665 |
. . . 4
⊢ ({𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} = {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} → (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) = (𝑥 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} ↦ (2nd
‘𝑥))) |
23 | 21, 22 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) = (𝑥 ∈ {𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) |
24 | 10, 13, 23 | wlkiswwlkbij 26248 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)):{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) |
25 | | f1oeq1 6040 |
. . 3
⊢ (𝑓 = (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) → (𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} ↔ (𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)):{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) |
26 | 25 | spcegv 3267 |
. 2
⊢ ((𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)) ∈ V →
((𝑥 ∈ {𝑡 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑡)) = 𝑁 ∧ ((2nd
‘𝑡)‘0) = 𝑃)} ↦ (2nd
‘𝑥)):{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃} → ∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃})) |
27 | 2, 24, 26 | mpsyl 66 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
∃𝑓 𝑓:{𝑝 ∈ (𝑉 Walks 𝐸) ∣ ((#‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑃}) |