Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . . 6
β’ (π = πΊ β (WWalksβπ) = (WWalksβπΊ)) |
2 | 1 | adantl 480 |
. . . . 5
β’ ((π = π β§ π = πΊ) β (WWalksβπ) = (WWalksβπΊ)) |
3 | | oveq1 7420 |
. . . . . . 7
β’ (π = π β (π + 1) = (π + 1)) |
4 | 3 | eqeq2d 2741 |
. . . . . 6
β’ (π = π β ((β―βπ€) = (π + 1) β (β―βπ€) = (π + 1))) |
5 | 4 | adantr 479 |
. . . . 5
β’ ((π = π β§ π = πΊ) β ((β―βπ€) = (π + 1) β (β―βπ€) = (π + 1))) |
6 | 2, 5 | rabeqbidv 3447 |
. . . 4
β’ ((π = π β§ π = πΊ) β {π€ β (WWalksβπ) β£ (β―βπ€) = (π + 1)} = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
7 | | df-wwlksn 29350 |
. . . 4
β’ WWalksN
= (π β
β0, π
β V β¦ {π€ β
(WWalksβπ) β£
(β―βπ€) = (π + 1)}) |
8 | | fvex 6905 |
. . . . 5
β’
(WWalksβπΊ)
β V |
9 | 8 | rabex 5333 |
. . . 4
β’ {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)} β V |
10 | 6, 7, 9 | ovmpoa 7567 |
. . 3
β’ ((π β β0
β§ πΊ β V) β
(π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
11 | 10 | expcom 412 |
. 2
β’ (πΊ β V β (π β β0
β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)})) |
12 | 7 | reldmmpo 7547 |
. . . . 5
β’ Rel dom
WWalksN |
13 | 12 | ovprc2 7453 |
. . . 4
β’ (Β¬
πΊ β V β (π WWalksN πΊ) = β
) |
14 | | fvprc 6884 |
. . . . . 6
β’ (Β¬
πΊ β V β
(WWalksβπΊ) =
β
) |
15 | 14 | rabeqdv 3445 |
. . . . 5
β’ (Β¬
πΊ β V β {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)} = {π€ β β
β£ (β―βπ€) = (π + 1)}) |
16 | | rab0 4383 |
. . . . 5
β’ {π€ β β
β£
(β―βπ€) = (π + 1)} =
β
|
17 | 15, 16 | eqtrdi 2786 |
. . . 4
β’ (Β¬
πΊ β V β {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)} = β
) |
18 | 13, 17 | eqtr4d 2773 |
. . 3
β’ (Β¬
πΊ β V β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
19 | 18 | a1d 25 |
. 2
β’ (Β¬
πΊ β V β (π β β0
β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)})) |
20 | 11, 19 | pm2.61i 182 |
1
β’ (π β β0
β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |