Step | Hyp | Ref
| Expression |
1 | | clwlkwlk 28765 |
. . . . . . . 8
β’ (π€ β (ClWalksβπΊ) β π€ β (WalksβπΊ)) |
2 | | wlkop 28618 |
. . . . . . . 8
β’ (π€ β (WalksβπΊ) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π€ β (ClWalksβπΊ) β π€ = β¨(1st βπ€), (2nd βπ€)β©) |
4 | | fvex 6860 |
. . . . . . . . . . . . . . 15
β’
(1st βπ€) β V |
5 | | hasheq0 14270 |
. . . . . . . . . . . . . . 15
β’
((1st βπ€) β V β
((β―β(1st βπ€)) = 0 β (1st βπ€) = β
)) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
((β―β(1st βπ€)) = 0 β (1st βπ€) = β
) |
7 | 6 | biimpi 215 |
. . . . . . . . . . . . 13
β’
((β―β(1st βπ€)) = 0 β (1st βπ€) = β
) |
8 | 7 | adantr 482 |
. . . . . . . . . . . 12
β’
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β (1st βπ€) = β
) |
9 | 8 | 3ad2ant3 1136 |
. . . . . . . . . . 11
β’ ((π β π β§ (1st βπ€)(ClWalksβπΊ)(2nd βπ€) β§
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)) β (1st βπ€) = β
) |
10 | 8 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β (1st βπ€) = β
) |
11 | 10 | breq1d 5120 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β
β
(ClWalksβπΊ)(2nd βπ€))) |
12 | | clwlknon2num.v |
. . . . . . . . . . . . . . . . . . 19
β’ π = (VtxβπΊ) |
13 | 12 | 1vgrex 27995 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β πΊ β V) |
14 | 12 | 0clwlk 29116 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β V β
(β
(ClWalksβπΊ)(2nd βπ€) β (2nd βπ€):(0...0)βΆπ)) |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β (β
(ClWalksβπΊ)(2nd βπ€) β (2nd
βπ€):(0...0)βΆπ)) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β (β
(ClWalksβπΊ)(2nd βπ€) β (2nd
βπ€):(0...0)βΆπ)) |
17 | 11, 16 | bitrd 279 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β (2nd
βπ€):(0...0)βΆπ)) |
18 | | fz0sn 13548 |
. . . . . . . . . . . . . . . . 17
β’ (0...0) =
{0} |
19 | 18 | feq2i 6665 |
. . . . . . . . . . . . . . . 16
β’
((2nd βπ€):(0...0)βΆπ β (2nd βπ€):{0}βΆπ) |
20 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . 18
β’ 0 β
V |
21 | 20 | fsn2 7087 |
. . . . . . . . . . . . . . . . 17
β’
((2nd βπ€):{0}βΆπ β (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) |
22 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β§ (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) β (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©}) |
23 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((2nd βπ€)β0) = π) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β§ (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) β ((2nd
βπ€)β0) = π) |
25 | 24 | opeq2d 4842 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β§ (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) β β¨0,
((2nd βπ€)β0)β© = β¨0, πβ©) |
26 | 25 | sneqd 4603 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β§ (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) β {β¨0,
((2nd βπ€)β0)β©} = {β¨0, πβ©}) |
27 | 22, 26 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β§ (((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©})) β (2nd
βπ€) = {β¨0, πβ©}) |
28 | 27 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((((2nd βπ€)β0) β π β§ (2nd
βπ€) = {β¨0,
((2nd βπ€)β0)β©}) β (2nd
βπ€) = {β¨0, πβ©})) |
29 | 21, 28 | biimtrid 241 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((2nd βπ€):{0}βΆπ β (2nd βπ€) = {β¨0, πβ©})) |
30 | 19, 29 | biimtrid 241 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((2nd βπ€):(0...0)βΆπ β (2nd
βπ€) = {β¨0, πβ©})) |
31 | 17, 30 | sylbid 239 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β (2nd
βπ€) = {β¨0, πβ©})) |
32 | 31 | ex 414 |
. . . . . . . . . . . . 13
β’ (π β π β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β (2nd
βπ€) = {β¨0, πβ©}))) |
33 | 32 | com23 86 |
. . . . . . . . . . . 12
β’ (π β π β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β (2nd βπ€) = {β¨0, πβ©}))) |
34 | 33 | 3imp 1112 |
. . . . . . . . . . 11
β’ ((π β π β§ (1st βπ€)(ClWalksβπΊ)(2nd βπ€) β§
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)) β (2nd βπ€) = {β¨0, πβ©}) |
35 | 9, 34 | opeq12d 4843 |
. . . . . . . . . 10
β’ ((π β π β§ (1st βπ€)(ClWalksβπΊ)(2nd βπ€) β§
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)) β β¨(1st βπ€), (2nd βπ€)β© = β¨β
,
{β¨0, πβ©}β©) |
36 | 35 | 3exp 1120 |
. . . . . . . . 9
β’ (π β π β ((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β β¨(1st βπ€), (2nd βπ€)β© = β¨β
,
{β¨0, πβ©}β©))) |
37 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
(π€ β
(ClWalksβπΊ) β
β¨(1st βπ€), (2nd βπ€)β© β (ClWalksβπΊ))) |
38 | | df-br 5111 |
. . . . . . . . . . 11
β’
((1st βπ€)(ClWalksβπΊ)(2nd βπ€) β β¨(1st βπ€), (2nd βπ€)β© β
(ClWalksβπΊ)) |
39 | 37, 38 | bitr4di 289 |
. . . . . . . . . 10
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
(π€ β
(ClWalksβπΊ) β
(1st βπ€)(ClWalksβπΊ)(2nd βπ€))) |
40 | | eqeq1 2741 |
. . . . . . . . . . 11
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
(π€ = β¨β
,
{β¨0, πβ©}β©
β β¨(1st βπ€), (2nd βπ€)β© = β¨β
, {β¨0, πβ©}β©)) |
41 | 40 | imbi2d 341 |
. . . . . . . . . 10
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
((((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©) β
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β β¨(1st βπ€), (2nd βπ€)β© = β¨β
,
{β¨0, πβ©}β©))) |
42 | 39, 41 | imbi12d 345 |
. . . . . . . . 9
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
((π€ β
(ClWalksβπΊ) β
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©)) β ((1st
βπ€)(ClWalksβπΊ)(2nd βπ€) β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β β¨(1st βπ€), (2nd βπ€)β© = β¨β
,
{β¨0, πβ©}β©)))) |
43 | 36, 42 | syl5ibr 246 |
. . . . . . . 8
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
(π β π β (π€ β (ClWalksβπΊ) β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©)))) |
44 | 43 | com23 86 |
. . . . . . 7
β’ (π€ = β¨(1st
βπ€), (2nd
βπ€)β© β
(π€ β
(ClWalksβπΊ) β
(π β π β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©)))) |
45 | 3, 44 | mpcom 38 |
. . . . . 6
β’ (π€ β (ClWalksβπΊ) β (π β π β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©))) |
46 | 45 | com12 32 |
. . . . 5
β’ (π β π β (π€ β (ClWalksβπΊ) β (((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π) β π€ = β¨β
, {β¨0, πβ©}β©))) |
47 | 46 | impd 412 |
. . . 4
β’ (π β π β ((π€ β (ClWalksβπΊ) β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β π€ = β¨β
, {β¨0, πβ©}β©)) |
48 | | eqidd 2738 |
. . . . . . 7
β’ (π β π β β
= β
) |
49 | 20 | a1i 11 |
. . . . . . . 8
β’ (π β π β 0 β V) |
50 | | snidg 4625 |
. . . . . . . 8
β’ (π β π β π β {π}) |
51 | 49, 50 | fsnd 6832 |
. . . . . . 7
β’ (π β π β {β¨0, πβ©}:{0}βΆ{π}) |
52 | 12 | 0clwlkv 29117 |
. . . . . . 7
β’ ((π β π β§ β
= β
β§ {β¨0,
πβ©}:{0}βΆ{π}) β
β
(ClWalksβπΊ){β¨0, πβ©}) |
53 | 48, 51, 52 | mpd3an23 1464 |
. . . . . 6
β’ (π β π β β
(ClWalksβπΊ){β¨0, πβ©}) |
54 | | hash0 14274 |
. . . . . . 7
β’
(β―ββ
) = 0 |
55 | 54 | a1i 11 |
. . . . . 6
β’ (π β π β (β―ββ
) =
0) |
56 | | fvsng 7131 |
. . . . . . 7
β’ ((0
β V β§ π β
π) β ({β¨0, πβ©}β0) = π) |
57 | 20, 56 | mpan 689 |
. . . . . 6
β’ (π β π β ({β¨0, πβ©}β0) = π) |
58 | 53, 55, 57 | jca32 517 |
. . . . 5
β’ (π β π β (β
(ClWalksβπΊ){β¨0, πβ©} β§ ((β―ββ
) = 0
β§ ({β¨0, πβ©}β0) = π))) |
59 | | eleq1 2826 |
. . . . . . 7
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(π€ β
(ClWalksβπΊ) β
β¨β
, {β¨0, πβ©}β© β (ClWalksβπΊ))) |
60 | | df-br 5111 |
. . . . . . 7
β’
(β
(ClWalksβπΊ){β¨0, πβ©} β β¨β
, {β¨0,
πβ©}β© β
(ClWalksβπΊ)) |
61 | 59, 60 | bitr4di 289 |
. . . . . 6
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(π€ β
(ClWalksβπΊ) β
β
(ClWalksβπΊ){β¨0, πβ©})) |
62 | | 0ex 5269 |
. . . . . . . . 9
β’ β
β V |
63 | | snex 5393 |
. . . . . . . . 9
β’ {β¨0,
πβ©} β
V |
64 | 62, 63 | op1std 7936 |
. . . . . . . 8
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(1st βπ€) =
β
) |
65 | 64 | fveqeq2d 6855 |
. . . . . . 7
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
((β―β(1st βπ€)) = 0 β (β―ββ
) =
0)) |
66 | 62, 63 | op2ndd 7937 |
. . . . . . . . 9
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(2nd βπ€) =
{β¨0, πβ©}) |
67 | 66 | fveq1d 6849 |
. . . . . . . 8
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
((2nd βπ€)β0) = ({β¨0, πβ©}β0)) |
68 | 67 | eqeq1d 2739 |
. . . . . . 7
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(((2nd βπ€)β0) = π β ({β¨0, πβ©}β0) = π)) |
69 | 65, 68 | anbi12d 632 |
. . . . . 6
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
(((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π) β ((β―ββ
) = 0 β§
({β¨0, πβ©}β0) = π))) |
70 | 61, 69 | anbi12d 632 |
. . . . 5
β’ (π€ = β¨β
, {β¨0,
πβ©}β© β
((π€ β
(ClWalksβπΊ) β§
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)) β (β
(ClWalksβπΊ){β¨0, πβ©} β§ ((β―ββ
) = 0
β§ ({β¨0, πβ©}β0) = π)))) |
71 | 58, 70 | syl5ibrcom 247 |
. . . 4
β’ (π β π β (π€ = β¨β
, {β¨0, πβ©}β© β (π€ β (ClWalksβπΊ) β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)))) |
72 | 47, 71 | impbid 211 |
. . 3
β’ (π β π β ((π€ β (ClWalksβπΊ) β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β π€ = β¨β
, {β¨0, πβ©}β©)) |
73 | 72 | alrimiv 1931 |
. 2
β’ (π β π β βπ€((π€ β (ClWalksβπΊ) β§ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)) β π€ = β¨β
, {β¨0, πβ©}β©)) |
74 | | rabeqsn 4632 |
. 2
β’ ({π€ β (ClWalksβπΊ) β£
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)} = {β¨β
, {β¨0, πβ©}β©} β
βπ€((π€ β (ClWalksβπΊ) β§
((β―β(1st βπ€)) = 0 β§ ((2nd βπ€)β0) = π)) β π€ = β¨β
, {β¨0, πβ©}β©)) |
75 | 73, 74 | sylibr 233 |
1
β’ (π β π β {π€ β (ClWalksβπΊ) β£ ((β―β(1st
βπ€)) = 0 β§
((2nd βπ€)β0) = π)} = {β¨β
, {β¨0, πβ©}β©}) |