Step | Hyp | Ref
| Expression |
1 | | 0ov 7394 |
. . 3
β’ (π΄β
π΅) = β
|
2 | | df-wwlksnon 28777 |
. . . . 5
β’
WWalksNOn = (π β
β0, π
β V β¦ (π β
(Vtxβπ), π β (Vtxβπ) β¦ {π€ β (π WWalksN π) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
3 | 2 | mpondm0 7594 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π
WWalksNOn πΊ) =
β
) |
4 | 3 | oveqd 7374 |
. . 3
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = (π΄β
π΅)) |
5 | | df-wwlksn 28776 |
. . . . . 6
β’ WWalksN
= (π β
β0, π
β V β¦ {π€ β
(WWalksβπ) β£
(β―βπ€) = (π + 1)}) |
6 | 5 | mpondm0 7594 |
. . . . 5
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π WWalksN
πΊ) =
β
) |
7 | 6 | rabeqdv 3422 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β {π€ β
(π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = {π€ β β
β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
8 | | rab0 4342 |
. . . 4
β’ {π€ β β
β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
|
9 | 7, 8 | eqtrdi 2792 |
. . 3
β’ (Β¬
(π β
β0 β§ πΊ
β V) β {π€ β
(π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
) |
10 | 1, 4, 9 | 3eqtr4a 2802 |
. 2
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
11 | | iswwlksnon.v |
. . . . . . . . 9
β’ π = (VtxβπΊ) |
12 | 11 | wwlksnon 28796 |
. . . . . . . 8
β’ ((π β β0
β§ πΊ β V) β
(π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
13 | 12 | adantr 481 |
. . . . . . 7
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
14 | 13 | oveqd 7374 |
. . . . . 6
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅)) |
15 | | eqid 2736 |
. . . . . . . 8
β’ (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)}) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)}) |
16 | 15 | mpondm0 7594 |
. . . . . . 7
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅) = β
) |
17 | 16 | adantl 482 |
. . . . . 6
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})π΅) = β
) |
18 | 14, 17 | eqtrd 2776 |
. . . . 5
β’ (((π β β0
β§ πΊ β V) β§
Β¬ (π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
19 | 18 | ex 413 |
. . . 4
β’ ((π β β0
β§ πΊ β V) β
(Β¬ (π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
)) |
20 | 4, 1 | eqtrdi 2792 |
. . . . 5
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
21 | 20 | a1d 25 |
. . . 4
β’ (Β¬
(π β
β0 β§ πΊ
β V) β (Β¬ (π΄
β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
)) |
22 | 19, 21 | pm2.61i 182 |
. . 3
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = β
) |
23 | 11 | wwlknllvtx 28791 |
. . . . . . 7
β’ (π€ β (π WWalksN πΊ) β ((π€β0) β π β§ (π€βπ) β π)) |
24 | | eleq1 2825 |
. . . . . . . . 9
β’ (π΄ = (π€β0) β (π΄ β π β (π€β0) β π)) |
25 | 24 | eqcoms 2744 |
. . . . . . . 8
β’ ((π€β0) = π΄ β (π΄ β π β (π€β0) β π)) |
26 | | eleq1 2825 |
. . . . . . . . 9
β’ (π΅ = (π€βπ) β (π΅ β π β (π€βπ) β π)) |
27 | 26 | eqcoms 2744 |
. . . . . . . 8
β’ ((π€βπ) = π΅ β (π΅ β π β (π€βπ) β π)) |
28 | 25, 27 | bi2anan9 637 |
. . . . . . 7
β’ (((π€β0) = π΄ β§ (π€βπ) = π΅) β ((π΄ β π β§ π΅ β π) β ((π€β0) β π β§ (π€βπ) β π))) |
29 | 23, 28 | syl5ibrcom 246 |
. . . . . 6
β’ (π€ β (π WWalksN πΊ) β (((π€β0) = π΄ β§ (π€βπ) = π΅) β (π΄ β π β§ π΅ β π))) |
30 | 29 | con3rr3 155 |
. . . . 5
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π€ β (π WWalksN πΊ) β Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅))) |
31 | 30 | ralrimiv 3142 |
. . . 4
β’ (Β¬
(π΄ β π β§ π΅ β π) β βπ€ β (π WWalksN πΊ) Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅)) |
32 | | rabeq0 4344 |
. . . 4
β’ ({π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
β βπ€ β (π WWalksN πΊ) Β¬ ((π€β0) = π΄ β§ (π€βπ) = π΅)) |
33 | 31, 32 | sylibr 233 |
. . 3
β’ (Β¬
(π΄ β π β§ π΅ β π) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} = β
) |
34 | 22, 33 | eqtr4d 2779 |
. 2
β’ (Β¬
(π΄ β π β§ π΅ β π) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
35 | 12 | adantr 481 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β (π WWalksNOn πΊ) = (π β π, π β π β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)})) |
36 | | eqeq2 2748 |
. . . . . 6
β’ (π = π΄ β ((π€β0) = π β (π€β0) = π΄)) |
37 | | eqeq2 2748 |
. . . . . 6
β’ (π = π΅ β ((π€βπ) = π β (π€βπ) = π΅)) |
38 | 36, 37 | bi2anan9 637 |
. . . . 5
β’ ((π = π΄ β§ π = π΅) β (((π€β0) = π β§ (π€βπ) = π) β ((π€β0) = π΄ β§ (π€βπ) = π΅))) |
39 | 38 | rabbidv 3415 |
. . . 4
β’ ((π = π΄ β§ π = π΅) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
40 | 39 | adantl 482 |
. . 3
β’ ((((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β§ (π = π΄ β§ π = π΅)) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
41 | | simprl 769 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β π΄ β π) |
42 | | simprr 771 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β π΅ β π) |
43 | | ovex 7390 |
. . . . 5
β’ (π WWalksN πΊ) β V |
44 | 43 | rabex 5289 |
. . . 4
β’ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} β V |
45 | 44 | a1i 11 |
. . 3
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} β V) |
46 | 35, 40, 41, 42, 45 | ovmpod 7507 |
. 2
β’ (((π β β0
β§ πΊ β V) β§
(π΄ β π β§ π΅ β π)) β (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)}) |
47 | 10, 34, 46 | ecase 1031 |
1
β’ (π΄(π WWalksNOn πΊ)π΅) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π΄ β§ (π€βπ) = π΅)} |