Step | Hyp | Ref
| Expression |
1 | | dlwwlknondlwlknonbij.w |
. . . 4
β’ π = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π β§ ((2nd
βπ€)β(π β 2)) = π)} |
2 | | df-3an 1090 |
. . . . 5
β’
(((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π) β (((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π) β§ ((2nd
βπ€)β(π β 2)) = π)) |
3 | 2 | rabbii 3416 |
. . . 4
β’ {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π β§ ((2nd βπ€)β(π β 2)) = π)} = {π€ β (ClWalksβπΊ) β£ (((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π) β§ ((2nd
βπ€)β(π β 2)) = π)} |
4 | 1, 3 | eqtri 2765 |
. . 3
β’ π = {π€ β (ClWalksβπΊ) β£ (((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π) β§ ((2nd
βπ€)β(π β 2)) = π)} |
5 | | eqid 2737 |
. . 3
β’ {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} |
6 | | dlwwlknondlwlknonf1o.f |
. . 3
β’ πΉ = (π β π β¦ ((2nd βπ) prefix
(β―β(1st βπ)))) |
7 | | eqid 2737 |
. . 3
β’ (π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))) = (π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))) |
8 | | eluz2nn 12816 |
. . . 4
β’ (π β
(β€β₯β2) β π β β) |
9 | | dlwwlknondlwlknonbij.v |
. . . . 5
β’ π = (VtxβπΊ) |
10 | 9, 5, 7 | clwwlknonclwlknonf1o 29348 |
. . . 4
β’ ((πΊ β USPGraph β§ π β π β§ π β β) β (π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))):{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |
11 | 8, 10 | syl3an3 1166 |
. . 3
β’ ((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β (π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β¦ ((2nd βπ) prefix
(β―β(1st βπ)))):{π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |
12 | | fveq1 6846 |
. . . . . . 7
β’ (π¦ = ((2nd βπ) prefix
(β―β(1st βπ))) β (π¦β(π β 2)) = (((2nd
βπ) prefix
(β―β(1st βπ)))β(π β 2))) |
13 | 12 | 3ad2ant3 1136 |
. . . . . 6
β’ (((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β§ π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β§ π¦ = ((2nd βπ) prefix (β―β(1st
βπ)))) β (π¦β(π β 2)) = (((2nd
βπ) prefix
(β―β(1st βπ)))β(π β 2))) |
14 | | 2fveq3 6852 |
. . . . . . . . . . . . 13
β’ (π€ = π β (β―β(1st
βπ€)) =
(β―β(1st βπ))) |
15 | 14 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ (π€ = π β ((β―β(1st
βπ€)) = π β
(β―β(1st βπ)) = π)) |
16 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π€ = π β (2nd βπ€) = (2nd βπ)) |
17 | 16 | fveq1d 6849 |
. . . . . . . . . . . . 13
β’ (π€ = π β ((2nd βπ€)β0) = ((2nd
βπ)β0)) |
18 | 17 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ (π€ = π β (((2nd βπ€)β0) = π β ((2nd βπ)β0) = π)) |
19 | 15, 18 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π€ = π β (((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π) β
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π))) |
20 | 19 | elrab 3650 |
. . . . . . . . . 10
β’ (π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} β (π β (ClWalksβπΊ) β§ ((β―β(1st
βπ)) = π β§ ((2nd
βπ)β0) = π))) |
21 | | simplrl 776 |
. . . . . . . . . . . 12
β’ (((π β (ClWalksβπΊ) β§
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)) β§ (πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)))
β (β―β(1st βπ)) = π) |
22 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π β (ClWalksβπΊ) β§
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)) β§ (πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)))
β π β
(ClWalksβπΊ)) |
23 | | simpr3 1197 |
. . . . . . . . . . . 12
β’ (((π β (ClWalksβπΊ) β§
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)) β§ (πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)))
β π β
(β€β₯β2)) |
24 | 21, 22, 23 | 3jca 1129 |
. . . . . . . . . . 11
β’ (((π β (ClWalksβπΊ) β§
((β―β(1st βπ)) = π β§ ((2nd βπ)β0) = π)) β§ (πΊ β USPGraph β§ π β π β§ π β (β€β₯β2)))
β ((β―β(1st βπ)) = π β§ π β (ClWalksβπΊ) β§ π β
(β€β₯β2))) |
25 | 24 | ex 414 |
. . . . . . . . . 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 409 |
. . . . . . . 8
β’ (((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β§ π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)}) β ((β―β(1st
βπ)) = π β§ π β (ClWalksβπΊ) β§ π β
(β€β₯β2))) |
28 | | dlwwlknondlwlknonf1olem1 29350 |
. . . . . . . 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 1133 |
. . . . . 6
β’ (((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β§ π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β§ π¦ = ((2nd βπ) prefix (β―β(1st
βπ)))) β
(((2nd βπ)
prefix (β―β(1st βπ)))β(π β 2)) = ((2nd βπ)β(π β 2))) |
31 | 13, 30 | eqtrd 2777 |
. . . . 5
β’ (((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β§ π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β§ π¦ = ((2nd βπ) prefix (β―β(1st
βπ)))) β (π¦β(π β 2)) = ((2nd βπ)β(π β 2))) |
32 | 31 | eqeq1d 2739 |
. . . 4
β’ (((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β§ π β {π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = π β§ ((2nd βπ€)β0) = π)} β§ π¦ = ((2nd βπ) prefix (β―β(1st
βπ)))) β ((π¦β(π β 2)) = π β ((2nd βπ)β(π β 2)) = π)) |
33 | | nfv 1918 |
. . . . 5
β’
β²π€((2nd βπ)β(π β 2)) = π |
34 | 16 | fveq1d 6849 |
. . . . . 6
β’ (π€ = π β ((2nd βπ€)β(π β 2)) = ((2nd βπ)β(π β 2))) |
35 | 34 | eqeq1d 2739 |
. . . . 5
β’ (π€ = π β (((2nd βπ€)β(π β 2)) = π β ((2nd βπ)β(π β 2)) = π)) |
36 | 33, 35 | sbiev 2309 |
. . . 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 7079 |
. 2
β’ ((πΊ β USPGraph β§ π β π β§ π β (β€β₯β2))
β πΉ:πβ1-1-ontoβ{π¦ β (π(ClWWalksNOnβπΊ)π) β£ (π¦β(π β 2)) = π}) |
39 | | dlwwlknondlwlknonbij.d |
. . . 4
β’ π· = {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} |
40 | | fveq1 6846 |
. . . . . 6
β’ (π€ = π¦ β (π€β(π β 2)) = (π¦β(π β 2))) |
41 | 40 | eqeq1d 2739 |
. . . . 5
β’ (π€ = π¦ β ((π€β(π β 2)) = π β (π¦β(π β 2)) = π)) |
42 | 41 | cbvrabv 3420 |
. . . 4
β’ {π€ β (π(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π} = {π¦ β (π(ClWWalksNOnβπΊ)π) β£ (π¦β(π β 2)) = π} |
43 | 39, 42 | eqtri 2765 |
. . 3
β’ π· = {π¦ β (π(ClWWalksNOnβπΊ)π) β£ (π¦β(π β 2)) = π} |
44 | | f1oeq3 6779 |
. . 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βπ·) |