Step | Hyp | Ref
| Expression |
1 | | 0ov 7446 |
. . 3
β’ (π΄β
π΅) = β
|
2 | | df-wwlksnon 29086 |
. . . . 5
β’
WWalksNOn = (π β
β0, π
β V β¦ (π β
(Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π WWalksN π) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
3 | 2 | mpondm0 7647 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π
WWalksNOn πΊ) =
β
) |
4 | 3 | oveqd 7426 |
. . 3
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = (π΄β
π΅)) |
5 | | df-wwlksn 29085 |
. . . . . 6
β’ WWalksN
= (π β
β0, π
β V β¦ {π€ β
(WWalksβπ) β£
(β―βπ€) = (π + 1)}) |
6 | 5 | mpondm0 7647 |
. . . . 5
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π WWalksN
πΊ) =
β
) |
7 | 6 | rabeqdv 3448 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β {π€ β
(π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = {π€ β β
β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
8 | | rab0 4383 |
. . . 4
β’ {π€ β β
β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
|
9 | 7, 8 | eqtrdi 2789 |
. . 3
β’ (Β¬
(π β
β0 β§ πΊ
β V) β {π€ β
(π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
) |
10 | 1, 4, 9 | 3eqtr4a 2799 |
. 2
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
11 | | iswwlksnon.v |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
12 | 11 | wwlksnon 29105 |
. . . . . . . 8
β’ ((π β β0
β§ πΊ β V) β
(π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
14 | 13 | oveqd 7426 |
. . . . . 6
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅)) |
15 | | eqid 2733 |
. . . . . . . 8
β’ (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)}) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)}) |
16 | 15 | mpondm0 7647 |
. . . . . . 7
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅) = β
) |
17 | 16 | adantl 483 |
. . . . . 6
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅) = β
) |
18 | 14, 17 | eqtrd 2773 |
. . . . 5
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
19 | 18 | ex 414 |
. . . 4
β’ ((π β β0
β§ πΊ β V) β
(Β¬ (π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
)) |
20 | 4, 1 | eqtrdi 2789 |
. . . . 5
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
21 | 20 | a1d 25 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (Β¬ (π΄
β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
)) |
22 | 19, 21 | pm2.61i 182 |
. . 3
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
23 | 11 | wwlknllvtx 29100 |
. . . . . . 7
β’ (π€ β (π WWalksN πΊ) β ((π€β0) β π β§ (π€βπ) β π)) |
24 | | eleq1 2822 |
. . . . . . . . 9
β’ (π΄ = (π€β0) β (π΄ β π β (π€β0) β π)) |
25 | 24 | eqcoms 2741 |
. . . . . . . 8
β’ ((π€β0) = π΄ β (π΄ β π β (π€β0) β π)) |
26 | | eleq1 2822 |
. . . . . . . . 9
β’ (π΅ = (π€βπ) β (π΅ β π β (π€βπ) β π)) |
27 | 26 | eqcoms 2741 |
. . . . . . . 8
β’ ((π€βπ) = π΅ β (π΅ β π β (π€βπ) β π)) |
28 | 25, 27 | bi2anan9 638 |
. . . . . . 7
β’ (((π€β0) = π΄ β§ (π€βπ) = π΅) β ((π΄ β π β§ π΅ β π) β ((π€β0) β π β§ (π€βπ) β π))) |
29 | 23, 28 | syl5ibrcom 246 |
. . . . . 6
β’ (π€ β (π WWalksN πΊ) β (((π€β0) = π΄ β§ (π€βπ) = π΅) β (π΄ β π β§ π΅ β π))) |
30 | 29 | con3rr3 155 |
. . . . 5
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π€ β (π WWalksN πΊ) β Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅))) |
31 | 30 | ralrimiv 3146 |
. . . 4
β’ (Β¬
(π΄ β π β§ π΅ β π) β βπ€ β (π WWalksN πΊ) Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅)) |
32 | | rabeq0 4385 |
. . . 4
β’ ({π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
β βπ€ β (π WWalksN πΊ) Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅)) |
33 | 31, 32 | sylibr 233 |
. . 3
β’ (Β¬
(π΄ β π β§ π΅ β π) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
) |
34 | 22, 33 | eqtr4d 2776 |
. 2
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
35 | 12 | adantr 482 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β (π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
36 | | eqeq2 2745 |
. . . . . 6
β’ (π = π΄ β ((π€β0) = π β (π€β0) = π΄)) |
37 | | eqeq2 2745 |
. . . . . 6
β’ (π = π΅ β ((π€βπ) = π β (π€βπ) = π΅)) |
38 | 36, 37 | bi2anan9 638 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (((π€β0) = π β§ (π€βπ) = π) β ((π€β0) = π΄ β§ (π€βπ) = π΅))) |
39 | 38 | rabbidv 3441 |
. . . 4
β’ ((π = π΄ β§ π = π΅) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
40 | 39 | adantl 483 |
. . 3
β’ ((((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β§ (π = π΄ β§ π = π΅)) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
41 | | simprl 770 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β π΄ β π) |
42 | | simprr 772 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β π΅ β π) |
43 | | ovex 7442 |
. . . . 5
β’ (π WWalksN πΊ) β V |
44 | 43 | rabex 5333 |
. . . 4
β’ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} β V |
45 | 44 | a1i 11 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} β V) |
46 | 35, 40, 41, 42, 45 | ovmpod 7560 |
. 2
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
47 | 10, 34, 46 | ecase 1032 |
1
β’ (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} |