Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . . 5
β’ (π WWalksN πΊ) β V |
2 | 1 | mptrabex 7176 |
. . . 4
β’ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) β V |
3 | 2 | resex 5986 |
. . 3
β’ ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}) β V |
4 | | eqid 2733 |
. . . . . 6
β’ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) = (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) |
5 | | eqid 2733 |
. . . . . . 7
β’ {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} = {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} |
6 | 5, 4 | clwwlkf1o 29037 |
. . . . . 6
β’ (π β β β (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)):{π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)}β1-1-ontoβ(π ClWWalksN πΊ)) |
7 | | fveq1 6842 |
. . . . . . . . 9
β’ (π¦ = (π€ prefix π) β (π¦β0) = ((π€ prefix π)β0)) |
8 | 7 | eqeq1d 2735 |
. . . . . . . 8
β’ (π¦ = (π€ prefix π) β ((π¦β0) = π β ((π€ prefix π)β0) = π)) |
9 | 8 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ π¦ = (π€ prefix π)) β ((π¦β0) = π β ((π€ prefix π)β0) = π)) |
10 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (lastSβπ₯) = (lastSβπ€)) |
11 | | fveq1 6842 |
. . . . . . . . . . . . . 14
β’ (π₯ = π€ β (π₯β0) = (π€β0)) |
12 | 10, 11 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π₯ = π€ β ((lastSβπ₯) = (π₯β0) β (lastSβπ€) = (π€β0))) |
13 | 12 | elrab 3646 |
. . . . . . . . . . . 12
β’ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β (π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0))) |
14 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(VtxβπΊ) =
(VtxβπΊ) |
15 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(EdgβπΊ) =
(EdgβπΊ) |
16 | 14, 15 | wwlknp 28830 |
. . . . . . . . . . . . . 14
β’ (π€ β (π WWalksN πΊ) β (π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1) β§ βπ β (0..^π){(π€βπ), (π€β(π + 1))} β (EdgβπΊ))) |
17 | | simpll 766 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β§ π β β) β π€ β Word (VtxβπΊ)) |
18 | | nnz 12525 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β€) |
19 | | uzid 12783 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β π β
(β€β₯βπ)) |
20 | | peano2uz 12831 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π + 1) β
(β€β₯βπ)) |
22 | | elfz1end 13477 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β (1...π)) |
23 | 22 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β π β (1...π)) |
24 | | fzss2 13487 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β
(β€β₯βπ) β (1...π) β (1...(π + 1))) |
25 | 24 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π + 1) β
(β€β₯βπ) β§ π β (1...π)) β π β (1...(π + 1))) |
26 | 21, 23, 25 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β (1...(π + 1))) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β§ π β β) β π β (1...(π + 1))) |
28 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ€) =
(π + 1) β
(1...(β―βπ€)) =
(1...(π +
1))) |
29 | 28 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ€) =
(π + 1) β (π β
(1...(β―βπ€))
β π β (1...(π + 1)))) |
30 | 29 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β (π β (1...(β―βπ€)) β π β (1...(π + 1)))) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β§ π β β) β (π β (1...(β―βπ€)) β π β (1...(π + 1)))) |
32 | 27, 31 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β§ π β β) β π β (1...(β―βπ€))) |
33 | 17, 32 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β§ π β β) β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€)))) |
34 | 33 | ex 414 |
. . . . . . . . . . . . . . 15
β’ ((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1)) β (π β β β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))))) |
35 | 34 | 3adant3 1133 |
. . . . . . . . . . . . . 14
β’ ((π€ β Word (VtxβπΊ) β§ (β―βπ€) = (π + 1) β§ βπ β (0..^π){(π€βπ), (π€β(π + 1))} β (EdgβπΊ)) β (π β β β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))))) |
36 | 16, 35 | syl 17 |
. . . . . . . . . . . . 13
β’ (π€ β (π WWalksN πΊ) β (π β β β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))))) |
37 | 36 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β (π β β β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))))) |
38 | 13, 37 | sylbi 216 |
. . . . . . . . . . 11
β’ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β (π β β β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))))) |
39 | 38 | impcom 409 |
. . . . . . . . . 10
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)}) β (π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€)))) |
40 | | pfxfv0 14586 |
. . . . . . . . . 10
β’ ((π€ β Word (VtxβπΊ) β§ π β (1...(β―βπ€))) β ((π€ prefix π)β0) = (π€β0)) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)}) β ((π€ prefix π)β0) = (π€β0)) |
42 | 41 | eqeq1d 2735 |
. . . . . . . 8
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)}) β (((π€ prefix π)β0) = π β (π€β0) = π)) |
43 | 42 | 3adant3 1133 |
. . . . . . 7
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ π¦ = (π€ prefix π)) β (((π€ prefix π)β0) = π β (π€β0) = π)) |
44 | 9, 43 | bitrd 279 |
. . . . . 6
β’ ((π β β β§ π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ π¦ = (π€ prefix π)) β ((π¦β0) = π β (π€β0) = π)) |
45 | 4, 6, 44 | f1oresrab 7074 |
. . . . 5
β’ (π β β β ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ{π¦ β (π ClWWalksN πΊ) β£ (π¦β0) = π}) |
46 | 45 | adantl 483 |
. . . 4
β’ ((π β π β§ π β β) β ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ{π¦ β (π ClWWalksN πΊ) β£ (π¦β0) = π}) |
47 | | clwwlknon 29076 |
. . . . . 6
β’ (π(ClWWalksNOnβπΊ)π) = {π¦ β (π ClWWalksN πΊ) β£ (π¦β0) = π} |
48 | 47 | a1i 11 |
. . . . 5
β’ ((π β π β§ π β β) β (π(ClWWalksNOnβπΊ)π) = {π¦ β (π ClWWalksN πΊ) β£ (π¦β0) = π}) |
49 | 48 | f1oeq3d 6782 |
. . . 4
β’ ((π β π β§ π β β) β (((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ{π¦ β (π ClWWalksN πΊ) β£ (π¦β0) = π})) |
50 | 46, 49 | mpbird 257 |
. . 3
β’ ((π β π β§ π β β) β ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |
51 | | f1oeq1 6773 |
. . . 4
β’ (π = ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}) β (π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β ((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π))) |
52 | 51 | spcegv 3555 |
. . 3
β’ (((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}) β V β (((π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β¦ (π€ prefix π)) βΎ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}):{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β βπ π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π))) |
53 | 3, 50, 52 | mpsyl 68 |
. 2
β’ ((π β π β§ π β β) β βπ π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |
54 | | df-rab 3407 |
. . . . 5
β’ {π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)} = {π€ β£ (π€ β (π WWalksN πΊ) β§ ((lastSβπ€) = (π€β0) β§ (π€β0) = π))} |
55 | | anass 470 |
. . . . . . 7
β’ (((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π) β (π€ β (π WWalksN πΊ) β§ ((lastSβπ€) = (π€β0) β§ (π€β0) = π))) |
56 | 55 | bicomi 223 |
. . . . . 6
β’ ((π€ β (π WWalksN πΊ) β§ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)) β ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π)) |
57 | 56 | abbii 2803 |
. . . . 5
β’ {π€ β£ (π€ β (π WWalksN πΊ) β§ ((lastSβπ€) = (π€β0) β§ (π€β0) = π))} = {π€ β£ ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π)} |
58 | 13 | bicomi 223 |
. . . . . . . 8
β’ ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)}) |
59 | 58 | anbi1i 625 |
. . . . . . 7
β’ (((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π) β (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ (π€β0) = π)) |
60 | 59 | abbii 2803 |
. . . . . 6
β’ {π€ β£ ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π)} = {π€ β£ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ (π€β0) = π)} |
61 | | df-rab 3407 |
. . . . . 6
β’ {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π} = {π€ β£ (π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β§ (π€β0) = π)} |
62 | 60, 61 | eqtr4i 2764 |
. . . . 5
β’ {π€ β£ ((π€ β (π WWalksN πΊ) β§ (lastSβπ€) = (π€β0)) β§ (π€β0) = π)} = {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π} |
63 | 54, 57, 62 | 3eqtri 2765 |
. . . 4
β’ {π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)} = {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π} |
64 | | f1oeq2 6774 |
. . . 4
β’ ({π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)} = {π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π} β (π:{π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π))) |
65 | 63, 64 | mp1i 13 |
. . 3
β’ ((π β π β§ π β β) β (π:{π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π))) |
66 | 65 | exbidv 1925 |
. 2
β’ ((π β π β§ π β β) β (βπ π:{π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π) β βπ π:{π€ β {π₯ β (π WWalksN πΊ) β£ (lastSβπ₯) = (π₯β0)} β£ (π€β0) = π}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π))) |
67 | 53, 66 | mpbird 257 |
1
β’ ((π β π β§ π β β) β βπ π:{π€ β (π WWalksN πΊ) β£ ((lastSβπ€) = (π€β0) β§ (π€β0) = π)}β1-1-ontoβ(π(ClWWalksNOnβπΊ)π)) |