Step | Hyp | Ref
| Expression |
1 | | dlwwlknondlwlknonbij.w |
. . . 4
⊢ 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋 ∧ ((2nd
‘𝑤)‘(𝑁 − 2)) = 𝑋)} |
2 | | df-3an 1088 |
. . . . 5
⊢
(((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋) ↔ (((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋) ∧ ((2nd
‘𝑤)‘(𝑁 − 2)) = 𝑋)) |
3 | 2 | rabbii 3406 |
. . . 4
⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)} = {𝑤 ∈ (ClWalks‘𝐺) ∣ (((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋) ∧ ((2nd
‘𝑤)‘(𝑁 − 2)) = 𝑋)} |
4 | 1, 3 | eqtri 2768 |
. . 3
⊢ 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋) ∧ ((2nd
‘𝑤)‘(𝑁 − 2)) = 𝑋)} |
5 | | eqid 2740 |
. . 3
⊢ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} |
6 | | dlwwlknondlwlknonf1o.f |
. . 3
⊢ 𝐹 = (𝑐 ∈ 𝑊 ↦ ((2nd ‘𝑐) prefix
(♯‘(1st ‘𝑐)))) |
7 | | eqid 2740 |
. . 3
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ↦ ((2nd
‘𝑐) prefix
(♯‘(1st ‘𝑐)))) = (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ↦ ((2nd
‘𝑐) prefix
(♯‘(1st ‘𝑐)))) |
8 | | eluz2nn 12623 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℕ) |
9 | | dlwwlknondlwlknonbij.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
10 | 9, 5, 7 | clwwlknonclwlknonf1o 28722 |
. . . 4
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ↦ ((2nd
‘𝑐) prefix
(♯‘(1st ‘𝑐)))):{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁)) |
11 | 8, 10 | syl3an3 1164 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ↦ ((2nd ‘𝑐) prefix
(♯‘(1st ‘𝑐)))):{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁)) |
12 | | fveq1 6770 |
. . . . . . 7
⊢ (𝑦 = ((2nd ‘𝑐) prefix
(♯‘(1st ‘𝑐))) → (𝑦‘(𝑁 − 2)) = (((2nd
‘𝑐) prefix
(♯‘(1st ‘𝑐)))‘(𝑁 − 2))) |
13 | 12 | 3ad2ant3 1134 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))) → (𝑦‘(𝑁 − 2)) = (((2nd
‘𝑐) prefix
(♯‘(1st ‘𝑐)))‘(𝑁 − 2))) |
14 | | 2fveq3 6776 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → (♯‘(1st
‘𝑤)) =
(♯‘(1st ‘𝑐))) |
15 | 14 | eqeq1d 2742 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑐 → ((♯‘(1st
‘𝑤)) = 𝑁 ↔
(♯‘(1st ‘𝑐)) = 𝑁)) |
16 | | fveq2 6771 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑐 → (2nd ‘𝑤) = (2nd ‘𝑐)) |
17 | 16 | fveq1d 6773 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑐 → ((2nd ‘𝑤)‘0) = ((2nd
‘𝑐)‘0)) |
18 | 17 | eqeq1d 2742 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑐 → (((2nd ‘𝑤)‘0) = 𝑋 ↔ ((2nd ‘𝑐)‘0) = 𝑋)) |
19 | 15, 18 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑐 → (((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋) ↔
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋))) |
20 | 19 | elrab 3626 |
. . . . . . . . . 10
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ ((♯‘(1st
‘𝑐)) = 𝑁 ∧ ((2nd
‘𝑐)‘0) = 𝑋))) |
21 | | simplrl 774 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ (♯‘(1st ‘𝑐)) = 𝑁) |
22 | | simpll 764 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ 𝑐 ∈
(ClWalks‘𝐺)) |
23 | | simpr3 1195 |
. . . . . . . . . . . 12
⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ 𝑁 ∈
(ℤ≥‘2)) |
24 | 21, 22, 23 | 3jca 1127 |
. . . . . . . . . . 11
⊢ (((𝑐 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋)) ∧ (𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)))
→ ((♯‘(1st ‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈
(ℤ≥‘2))) |
25 | 24 | ex 413 |
. . . . . . . . . 10
⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧
((♯‘(1st ‘𝑐)) = 𝑁 ∧ ((2nd ‘𝑐)‘0) = 𝑋)) → ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(1st ‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈
(ℤ≥‘2)))) |
26 | 20, 25 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st
‘𝑤)) = 𝑁 ∧ ((2nd
‘𝑤)‘0) = 𝑋)} → ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ ((♯‘(1st ‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈
(ℤ≥‘2)))) |
27 | 26 | impcom 408 |
. . . . . . . 8
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)}) → ((♯‘(1st
‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈
(ℤ≥‘2))) |
28 | | dlwwlknondlwlknonf1olem1 28724 |
. . . . . . . 8
⊢
(((♯‘(1st ‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ≥‘2))
→ (((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))‘(𝑁 − 2)) = ((2nd
‘𝑐)‘(𝑁 − 2))) |
29 | 27, 28 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)}) → (((2nd ‘𝑐) prefix
(♯‘(1st ‘𝑐)))‘(𝑁 − 2)) = ((2nd ‘𝑐)‘(𝑁 − 2))) |
30 | 29 | 3adant3 1131 |
. . . . . 6
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))) →
(((2nd ‘𝑐)
prefix (♯‘(1st ‘𝑐)))‘(𝑁 − 2)) = ((2nd ‘𝑐)‘(𝑁 − 2))) |
31 | 13, 30 | eqtrd 2780 |
. . . . 5
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))) → (𝑦‘(𝑁 − 2)) = ((2nd ‘𝑐)‘(𝑁 − 2))) |
32 | 31 | eqeq1d 2742 |
. . . 4
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))) → ((𝑦‘(𝑁 − 2)) = 𝑋 ↔ ((2nd ‘𝑐)‘(𝑁 − 2)) = 𝑋)) |
33 | | nfv 1921 |
. . . . 5
⊢
Ⅎ𝑤((2nd ‘𝑐)‘(𝑁 − 2)) = 𝑋 |
34 | 16 | fveq1d 6773 |
. . . . . 6
⊢ (𝑤 = 𝑐 → ((2nd ‘𝑤)‘(𝑁 − 2)) = ((2nd ‘𝑐)‘(𝑁 − 2))) |
35 | 34 | eqeq1d 2742 |
. . . . 5
⊢ (𝑤 = 𝑐 → (((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋 ↔ ((2nd ‘𝑐)‘(𝑁 − 2)) = 𝑋)) |
36 | 33, 35 | sbiev 2313 |
. . . 4
⊢ ([𝑐 / 𝑤]((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋 ↔ ((2nd ‘𝑐)‘(𝑁 − 2)) = 𝑋) |
37 | 32, 36 | bitr4di 289 |
. . 3
⊢ (((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
∧ 𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣
((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ∧ 𝑦 = ((2nd ‘𝑐) prefix (♯‘(1st
‘𝑐)))) → ((𝑦‘(𝑁 − 2)) = 𝑋 ↔ [𝑐 / 𝑤]((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)) |
38 | 4, 5, 6, 7, 11, 37 | f1ossf1o 6997 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝐹:𝑊–1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋}) |
39 | | dlwwlknondlwlknonbij.d |
. . . 4
⊢ 𝐷 = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} |
40 | | fveq1 6770 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤‘(𝑁 − 2)) = (𝑦‘(𝑁 − 2))) |
41 | 40 | eqeq1d 2742 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝑤‘(𝑁 − 2)) = 𝑋 ↔ (𝑦‘(𝑁 − 2)) = 𝑋)) |
42 | 41 | cbvrabv 3425 |
. . . 4
⊢ {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋} = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋} |
43 | 39, 42 | eqtri 2768 |
. . 3
⊢ 𝐷 = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋} |
44 | | f1oeq3 6704 |
. . 3
⊢ (𝐷 = {𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋} → (𝐹:𝑊–1-1-onto→𝐷 ↔ 𝐹:𝑊–1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋})) |
45 | 43, 44 | ax-mp 5 |
. 2
⊢ (𝐹:𝑊–1-1-onto→𝐷 ↔ 𝐹:𝑊–1-1-onto→{𝑦 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑦‘(𝑁 − 2)) = 𝑋}) |
46 | 38, 45 | sylibr 233 |
1
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))
→ 𝐹:𝑊–1-1-onto→𝐷) |