Step | Hyp | Ref
| Expression |
1 | | fvex 6787 |
. . . . 5
⊢
(Walks‘𝐺)
∈ V |
2 | 1 | mptrabex 7101 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ∈
V |
3 | 2 | resex 5939 |
. . 3
⊢ ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}) ∈ V |
4 | | eqid 2738 |
. . . 4
⊢ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) = (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ↦ (2nd
‘𝑝)) |
5 | | eqid 2738 |
. . . . 5
⊢ {𝑞 ∈ (Walks‘𝐺) ∣
(♯‘(1st ‘𝑞)) = 𝑁} = {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} |
6 | | eqid 2738 |
. . . . 5
⊢ (𝑁 WWalksN 𝐺) = (𝑁 WWalksN 𝐺) |
7 | 5, 6, 4 | wlknwwlksnbij 28253 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(♯‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)):{𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁}–1-1-onto→(𝑁 WWalksN 𝐺)) |
8 | | fveq1 6773 |
. . . . . 6
⊢ (𝑤 = (2nd ‘𝑝) → (𝑤‘0) = ((2nd ‘𝑝)‘0)) |
9 | 8 | eqeq1d 2740 |
. . . . 5
⊢ (𝑤 = (2nd ‘𝑝) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
10 | 9 | 3ad2ant3 1134 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
∧ 𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(♯‘(1st ‘𝑞)) = 𝑁} ∧ 𝑤 = (2nd ‘𝑝)) → ((𝑤‘0) = 𝑋 ↔ ((2nd ‘𝑝)‘0) = 𝑋)) |
11 | 4, 7, 10 | f1oresrab 6999 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ ((𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣
(♯‘(1st ‘𝑞)) = 𝑁} ↦ (2nd ‘𝑝)) ↾ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}):{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
12 | | f1oeq1 6704 |
. . . 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) = 𝑋})) |
13 | 12 | spcegv 3536 |
. . 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) = 𝑋})) |
14 | 3, 11, 13 | mpsyl 68 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |
15 | | 2fveq3 6779 |
. . . . . . 7
⊢ (𝑝 = 𝑞 → (♯‘(1st
‘𝑝)) =
(♯‘(1st ‘𝑞))) |
16 | 15 | eqeq1d 2740 |
. . . . . 6
⊢ (𝑝 = 𝑞 → ((♯‘(1st
‘𝑝)) = 𝑁 ↔
(♯‘(1st ‘𝑞)) = 𝑁)) |
17 | 16 | rabrabi 3427 |
. . . . 5
⊢ {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} = {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)} |
18 | 17 | eqcomi 2747 |
. . . 4
⊢ {𝑝 ∈ (Walks‘𝐺) ∣
((♯‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)} = {𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋} |
19 | | f1oeq2 6705 |
. . . 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) = 𝑋})) |
20 | 18, 19 | mp1i 13 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ (𝑓:{𝑝 ∈ (Walks‘𝐺) ∣
((♯‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
21 | 20 | exbidv 1924 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ (∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} ↔ ∃𝑓 𝑓:{𝑝 ∈ {𝑞 ∈ (Walks‘𝐺) ∣ (♯‘(1st
‘𝑞)) = 𝑁} ∣ ((2nd
‘𝑝)‘0) = 𝑋}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋})) |
22 | 14, 21 | mpbird 256 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0)
→ ∃𝑓 𝑓:{𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st
‘𝑝)) = 𝑁 ∧ ((2nd
‘𝑝)‘0) = 𝑋)}–1-1-onto→{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑋}) |