Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | 1 | wlkonprop 28648 |
. . 3
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅))) |
3 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = 0 β (πβπ) = (πβ0)) |
4 | | fv0p1e1 12281 |
. . . . . . . . . . 11
β’ (π = 0 β (πβ(π + 1)) = (πβ1)) |
5 | 3, 4 | preq12d 4703 |
. . . . . . . . . 10
β’ (π = 0 β {(πβπ), (πβ(π + 1))} = {(πβ0), (πβ1)}) |
6 | 5 | sseq1d 3976 |
. . . . . . . . 9
β’ (π = 0 β ({(πβπ), (πβ(π + 1))} β π β {(πβ0), (πβ1)} β π)) |
7 | 6 | rexbidv 3172 |
. . . . . . . 8
β’ (π = 0 β (βπ β ran πΌ{(πβπ), (πβ(π + 1))} β π β βπ β ran πΌ{(πβ0), (πβ1)} β π)) |
8 | | wlkonl1iedg.i |
. . . . . . . . . . 11
β’ πΌ = (iEdgβπΊ) |
9 | 8 | wlkvtxiedg 28615 |
. . . . . . . . . 10
β’ (πΉ(WalksβπΊ)π β βπ β (0..^(β―βπΉ))βπ β ran πΌ{(πβπ), (πβ(π + 1))} β π) |
10 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β βπ β (0..^(β―βπΉ))βπ β ran πΌ{(πβπ), (πβ(π + 1))} β π) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ (((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β§ (β―βπΉ) β 0) β βπ β (0..^(β―βπΉ))βπ β ran πΌ{(πβπ), (πβ(π + 1))} β π) |
12 | | wlkcl 28605 |
. . . . . . . . . . 11
β’ (πΉ(WalksβπΊ)π β (β―βπΉ) β
β0) |
13 | | elnnne0 12432 |
. . . . . . . . . . . . 13
β’
((β―βπΉ)
β β β ((β―βπΉ) β β0 β§
(β―βπΉ) β
0)) |
14 | 13 | simplbi2 502 |
. . . . . . . . . . . 12
β’
((β―βπΉ)
β β0 β ((β―βπΉ) β 0 β (β―βπΉ) β
β)) |
15 | | lbfzo0 13618 |
. . . . . . . . . . . 12
β’ (0 β
(0..^(β―βπΉ))
β (β―βπΉ)
β β) |
16 | 14, 15 | syl6ibr 252 |
. . . . . . . . . . 11
β’
((β―βπΉ)
β β0 β ((β―βπΉ) β 0 β 0 β
(0..^(β―βπΉ)))) |
17 | 12, 16 | syl 17 |
. . . . . . . . . 10
β’ (πΉ(WalksβπΊ)π β ((β―βπΉ) β 0 β 0 β
(0..^(β―βπΉ)))) |
18 | 17 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β ((β―βπΉ) β 0 β 0 β
(0..^(β―βπΉ)))) |
19 | 18 | imp 408 |
. . . . . . . 8
β’ (((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β§ (β―βπΉ) β 0) β 0 β
(0..^(β―βπΉ))) |
20 | 7, 11, 19 | rspcdva 3581 |
. . . . . . 7
β’ (((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β§ (β―βπΉ) β 0) β βπ β ran πΌ{(πβ0), (πβ1)} β π) |
21 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πβ0) β
V |
22 | | fvex 6856 |
. . . . . . . . . . 11
β’ (πβ1) β
V |
23 | 21, 22 | prss 4781 |
. . . . . . . . . 10
β’ (((πβ0) β π β§ (πβ1) β π) β {(πβ0), (πβ1)} β π) |
24 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ ((πβ0) = π΄ β ((πβ0) β π β π΄ β π)) |
25 | | ax-1 6 |
. . . . . . . . . . . . 13
β’ (π΄ β π β ((πβ1) β π β π΄ β π)) |
26 | 24, 25 | syl6bi 253 |
. . . . . . . . . . . 12
β’ ((πβ0) = π΄ β ((πβ0) β π β ((πβ1) β π β π΄ β π))) |
27 | 26 | adantl 483 |
. . . . . . . . . . 11
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β ((πβ0) β π β ((πβ1) β π β π΄ β π))) |
28 | 27 | impd 412 |
. . . . . . . . . 10
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β (((πβ0) β π β§ (πβ1) β π) β π΄ β π)) |
29 | 23, 28 | biimtrrid 242 |
. . . . . . . . 9
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β ({(πβ0), (πβ1)} β π β π΄ β π)) |
30 | 29 | reximdv 3164 |
. . . . . . . 8
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β (βπ β ran πΌ{(πβ0), (πβ1)} β π β βπ β ran πΌ π΄ β π)) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ (((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β§ (β―βπΉ) β 0) β (βπ β ran πΌ{(πβ0), (πβ1)} β π β βπ β ran πΌ π΄ β π)) |
32 | 20, 31 | mpd 15 |
. . . . . 6
β’ (((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β§ (β―βπΉ) β 0) β βπ β ran πΌ π΄ β π) |
33 | 32 | ex 414 |
. . . . 5
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄) β ((β―βπΉ) β 0 β βπ β ran πΌ π΄ β π)) |
34 | 33 | 3adant3 1133 |
. . . 4
β’ ((πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅) β ((β―βπΉ) β 0 β βπ β ran πΌ π΄ β π)) |
35 | 34 | 3ad2ant3 1136 |
. . 3
β’ (((πΊ β V β§ π΄ β (VtxβπΊ) β§ π΅ β (VtxβπΊ)) β§ (πΉ β V β§ π β V) β§ (πΉ(WalksβπΊ)π β§ (πβ0) = π΄ β§ (πβ(β―βπΉ)) = π΅)) β ((β―βπΉ) β 0 β βπ β ran πΌ π΄ β π)) |
36 | 2, 35 | syl 17 |
. 2
β’ (πΉ(π΄(WalksOnβπΊ)π΅)π β ((β―βπΉ) β 0 β βπ β ran πΌ π΄ β π)) |
37 | 36 | imp 408 |
1
β’ ((πΉ(π΄(WalksOnβπΊ)π΅)π β§ (β―βπΉ) β 0) β βπ β ran πΌ π΄ β π) |