Step | Hyp | Ref
| Expression |
1 | | clwwlknonclwlknonf1o.w |
. . 3
β’ π = {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = π β§ ((2nd
βπ€)β0) = π)} |
2 | | eqid 2737 |
. . 3
β’ {π€ β (ClWalksβπΊ) β£
(β―β(1st βπ€)) = π} = {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} |
3 | | clwwlknonclwlknonf1o.f |
. . 3
β’ πΉ = (π β π β¦ ((2nd βπ) prefix
(β―β(1st βπ)))) |
4 | | eqid 2737 |
. . 3
β’ (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))) = (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))) |
5 | | eqid 2737 |
. . . . 5
β’
(1st βπ) = (1st βπ) |
6 | | eqid 2737 |
. . . . 5
β’
(2nd βπ) = (2nd βπ) |
7 | 5, 6, 2, 4 | clwlknf1oclwwlkn 29070 |
. . . 4
β’ ((πΊ β USPGraph β§ π β β) β (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))):{π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π}β1-1-ontoβ(π ClWWalksN πΊ)) |
8 | 7 | 3adant2 1132 |
. . 3
β’ ((πΊ β USPGraph β§ π β π β§ π β β) β (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β¦ ((2nd
βπ) prefix
(β―β(1st βπ)))):{π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π}β1-1-ontoβ(π ClWWalksN πΊ)) |
9 | | fveq1 6846 |
. . . . . . 7
β’ (π = ((2nd βπ) prefix
(β―β(1st βπ))) β (π β0) = (((2nd βπ) prefix
(β―β(1st βπ)))β0)) |
10 | 9 | 3ad2ant3 1136 |
. . . . . 6
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β§ π = ((2nd βπ) prefix (β―β(1st
βπ)))) β (π β0) = (((2nd
βπ) prefix
(β―β(1st βπ)))β0)) |
11 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π€ = π β (β―β(1st
βπ€)) =
(β―β(1st βπ))) |
12 | 11 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π€ = π β ((β―β(1st
βπ€)) = π β
(β―β(1st βπ)) = π)) |
13 | 12 | elrab 3650 |
. . . . . . . . . 10
β’ (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β (π β (ClWalksβπΊ) β§ (β―β(1st
βπ)) = π)) |
14 | | clwlkwlk 28765 |
. . . . . . . . . . . 12
β’ (π β (ClWalksβπΊ) β π β (WalksβπΊ)) |
15 | | wlkcpr 28619 |
. . . . . . . . . . . . 13
β’ (π β (WalksβπΊ) β (1st
βπ)(WalksβπΊ)(2nd βπ)) |
16 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(VtxβπΊ) =
(VtxβπΊ) |
17 | 16 | wlkpwrd 28607 |
. . . . . . . . . . . . . . . 16
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (2nd βπ) β Word (VtxβπΊ)) |
18 | 17 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β (2nd
βπ) β Word
(VtxβπΊ)) |
19 | | elnnuz 12814 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
(β€β₯β1)) |
20 | | eluzfz2 13456 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β1) β π β (1...π)) |
21 | 19, 20 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β (1...π)) |
22 | | fzelp1 13500 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β π β (1...(π + 1))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β (1...(π + 1))) |
24 | 23 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΊ β USPGraph β§ π β π β§ π β β) β π β (1...(π + 1))) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . 17
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β π β (1...(π + 1))) |
26 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―β(1st βπ)) = π β (β―β(1st
βπ)) = π) |
27 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―β(1st βπ)) = π β ((β―β(1st
βπ)) + 1) = (π + 1)) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―β(1st βπ)) = π β (1...((β―β(1st
βπ)) + 1)) =
(1...(π +
1))) |
29 | 26, 28 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . 18
β’
((β―β(1st βπ)) = π β ((β―β(1st
βπ)) β
(1...((β―β(1st βπ)) + 1)) β π β (1...(π + 1)))) |
30 | 29 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β
((β―β(1st βπ)) β
(1...((β―β(1st βπ)) + 1)) β π β (1...(π + 1)))) |
31 | 25, 30 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β
(β―β(1st βπ)) β
(1...((β―β(1st βπ)) + 1))) |
32 | | wlklenvp1 28608 |
. . . . . . . . . . . . . . . . . . 19
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (β―β(2nd
βπ)) =
((β―β(1st βπ)) + 1)) |
33 | 32 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . 18
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β (1...(β―β(2nd
βπ))) =
(1...((β―β(1st βπ)) + 1))) |
34 | 33 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((β―β(1st
βπ)) β
(1...(β―β(2nd βπ))) β (β―β(1st
βπ)) β
(1...((β―β(1st βπ)) + 1)))) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . 16
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β
((β―β(1st βπ)) β (1...(β―β(2nd
βπ))) β
(β―β(1st βπ)) β
(1...((β―β(1st βπ)) + 1)))) |
36 | 31, 35 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β
(β―β(1st βπ)) β (1...(β―β(2nd
βπ)))) |
37 | 18, 36 | jca 513 |
. . . . . . . . . . . . . 14
β’
(((1st βπ)(WalksβπΊ)(2nd βπ) β§ (β―β(1st
βπ)) = π β§ (πΊ β USPGraph β§ π β π β§ π β β)) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ))))) |
38 | 37 | 3exp 1120 |
. . . . . . . . . . . . 13
β’
((1st βπ)(WalksβπΊ)(2nd βπ) β ((β―β(1st
βπ)) = π β ((πΊ β USPGraph β§ π β π β§ π β β) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ))))))) |
39 | 15, 38 | sylbi 216 |
. . . . . . . . . . . 12
β’ (π β (WalksβπΊ) β
((β―β(1st βπ)) = π β ((πΊ β USPGraph β§ π β π β§ π β β) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ))))))) |
40 | 14, 39 | syl 17 |
. . . . . . . . . . 11
β’ (π β (ClWalksβπΊ) β
((β―β(1st βπ)) = π β ((πΊ β USPGraph β§ π β π β§ π β β) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ))))))) |
41 | 40 | imp 408 |
. . . . . . . . . 10
β’ ((π β (ClWalksβπΊ) β§
(β―β(1st βπ)) = π) β ((πΊ β USPGraph β§ π β π β§ π β β) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ)))))) |
42 | 13, 41 | sylbi 216 |
. . . . . . . . 9
β’ (π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β ((πΊ β USPGraph β§ π β π β§ π β β) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ)))))) |
43 | 42 | impcom 409 |
. . . . . . . 8
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π}) β ((2nd
βπ) β Word
(VtxβπΊ) β§
(β―β(1st βπ)) β (1...(β―β(2nd
βπ))))) |
44 | | pfxfv0 14587 |
. . . . . . . 8
β’
(((2nd βπ) β Word (VtxβπΊ) β§ (β―β(1st
βπ)) β
(1...(β―β(2nd βπ)))) β (((2nd βπ) prefix
(β―β(1st βπ)))β0) = ((2nd βπ)β0)) |
45 | 43, 44 | syl 17 |
. . . . . . 7
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π}) β (((2nd
βπ) prefix
(β―β(1st βπ)))β0) = ((2nd βπ)β0)) |
46 | 45 | 3adant3 1133 |
. . . . . 6
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β§ π = ((2nd βπ) prefix (β―β(1st
βπ)))) β
(((2nd βπ)
prefix (β―β(1st βπ)))β0) = ((2nd βπ)β0)) |
47 | 10, 46 | eqtrd 2777 |
. . . . 5
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β§ π = ((2nd βπ) prefix (β―β(1st
βπ)))) β (π β0) = ((2nd
βπ)β0)) |
48 | 47 | eqeq1d 2739 |
. . . 4
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β§ π = ((2nd βπ) prefix (β―β(1st
βπ)))) β ((π β0) = π β ((2nd βπ)β0) = π)) |
49 | | nfv 1918 |
. . . . 5
β’
β²π€((2nd βπ)β0) = π |
50 | | fveq2 6847 |
. . . . . . 7
β’ (π€ = π β (2nd βπ€) = (2nd βπ)) |
51 | 50 | fveq1d 6849 |
. . . . . 6
β’ (π€ = π β ((2nd βπ€)β0) = ((2nd
βπ)β0)) |
52 | 51 | eqeq1d 2739 |
. . . . 5
β’ (π€ = π β (((2nd βπ€)β0) = π β ((2nd βπ)β0) = π)) |
53 | 49, 52 | sbiev 2309 |
. . . 4
β’ ([π / π€]((2nd βπ€)β0) = π β ((2nd βπ)β0) = π) |
54 | 48, 53 | bitr4di 289 |
. . 3
β’ (((πΊ β USPGraph β§ π β π β§ π β β) β§ π β {π€ β (ClWalksβπΊ) β£ (β―β(1st
βπ€)) = π} β§ π = ((2nd βπ) prefix (β―β(1st
βπ)))) β ((π β0) = π β [π / π€]((2nd βπ€)β0) = π)) |
55 | 1, 2, 3, 4, 8, 54 | f1ossf1o 7079 |
. 2
β’ ((πΊ β USPGraph β§ π β π β§ π β β) β πΉ:πβ1-1-ontoβ{π β (π ClWWalksN πΊ) β£ (π β0) = π}) |
56 | | clwwlknon 29076 |
. . 3
β’ (π(ClWWalksNOnβπΊ)π) = {π β (π ClWWalksN πΊ) β£ (π β0) = π} |
57 | | f1oeq3 6779 |
. . 3
β’ ((π(ClWWalksNOnβπΊ)π) = {π β (π ClWWalksN πΊ) β£ (π β0) = π} β (πΉ:πβ1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β πΉ:πβ1-1-ontoβ{π β (π ClWWalksN πΊ) β£ (π β0) = π})) |
58 | 56, 57 | ax-mp 5 |
. 2
β’ (πΉ:πβ1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β πΉ:πβ1-1-ontoβ{π β (π ClWWalksN πΊ) β£ (π β0) = π}) |
59 | 55, 58 | sylibr 233 |
1
β’ ((πΊ β USPGraph β§ π β π β§ π β β) β πΉ:πβ1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |