Step | Hyp | Ref
| Expression |
1 | | wlkv 28602 |
. . 3
β’ (πΉ(WalksβπΊ)π β (πΊ β V β§ πΉ β V β§ π β V)) |
2 | | eqid 2733 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
3 | | eqid 2733 |
. . . . . . . . 9
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
4 | 2, 3 | iswlk 28600 |
. . . . . . . 8
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))))) |
5 | | simpr1 1195 |
. . . . . . . . . . 11
β’ ((((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) β πΉ β Word dom (iEdgβπΊ)) |
6 | | simpr2 1196 |
. . . . . . . . . . 11
β’ ((((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) β π:(0...(β―βπΉ))βΆ(VtxβπΊ)) |
7 | | df-ifp 1063 |
. . . . . . . . . . . . . . . . 17
β’
(if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) |
8 | | dfsn2 4600 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ {(πβπ)} = {(πβπ), (πβπ)} |
9 | | preq2 4696 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ) = (πβ(π + 1)) β {(πβπ), (πβπ)} = {(πβπ), (πβ(π + 1))}) |
10 | 8, 9 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πβπ) = (πβ(π + 1)) β {(πβπ)} = {(πβπ), (πβ(π + 1))}) |
11 | 10 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πβπ) = (πβ(π + 1)) β (((iEdgβπΊ)β(πΉβπ)) = {(πβπ)} β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
12 | 11 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
13 | 12 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β ((((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
14 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β πΊ β
UPGraph) |
15 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β πΉ β Word dom (iEdgβπΊ)) |
16 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(EdgβπΊ) =
(EdgβπΊ) |
17 | 3, 16 | upgredginwlk 28626 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πΊ β UPGraph β§ πΉ β Word dom
(iEdgβπΊ)) β
(π β
(0..^(β―βπΉ))
β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ))) |
18 | 14, 15, 17 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β (π β (0..^(β―βπΉ)) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ))) |
19 | 18 | imp 408 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) |
20 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β πΊ β UPGraph) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β πΊ β UPGraph) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β πΊ β UPGraph) |
23 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β πΊ β UPGraph) |
24 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) |
25 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) |
26 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β (πβ(π + 1)) β Β¬ (πβπ) = (πβ(π + 1))) |
27 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ) β (πβ(π + 1)) β (πβπ) β V) |
28 | | fvexd 6858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ) β (πβ(π + 1)) β (πβ(π + 1)) β V) |
29 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((πβπ) β (πβ(π + 1)) β (πβπ) β (πβ(π + 1))) |
30 | 27, 28, 29 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((πβπ) β (πβ(π + 1)) β ((πβπ) β V β§ (πβ(π + 1)) β V β§ (πβπ) β (πβ(π + 1)))) |
31 | 26, 30 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
(πβπ) = (πβ(π + 1)) β ((πβπ) β V β§ (πβ(π + 1)) β V β§ (πβπ) β (πβ(π + 1)))) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((Β¬
(πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((πβπ) β V β§ (πβ(π + 1)) β V β§ (πβπ) β (πβ(π + 1)))) |
33 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((πβπ) β V β§ (πβ(π + 1)) β V β§ (πβπ) β (πβ(π + 1)))) |
34 | 2, 16 | upgredgpr 28135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((πΊ β UPGraph β§
((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β§ ((πβπ) β V β§ (πβ(π + 1)) β V β§ (πβπ) β (πβ(π + 1)))) β {(πβπ), (πβ(π + 1))} = ((iEdgβπΊ)β(πΉβπ))) |
35 | 23, 24, 25, 33, 34 | syl31anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β {(πβπ), (πβ(π + 1))} = ((iEdgβπΊ)β(πΉβπ))) |
36 | 35 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((πΉ β Word
dom (iEdgβπΊ) β§
π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β§ ((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ)) β§ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
37 | 36 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β (((iEdgβπΊ)β(πΉβπ)) β (EdgβπΊ) β ((Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
38 | 19, 37 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Β¬
(πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
40 | 13, 39 | jaoi 856 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((((πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β ((((πβπ) = (πβ(π + 1)) β§ ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}) β¨ (Β¬ (πβπ) = (πβ(π + 1)) β§ {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
42 | 7, 41 | biimtrid 241 |
. . . . . . . . . . . . . . . 16
β’ ((((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β§ π β (0..^(β―βπΉ))) β (if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β ((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
43 | 42 | ralimdva 3161 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β§ ((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph)) β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
44 | 43 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
45 | 44 | com23 86 |
. . . . . . . . . . . . 13
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ)) β (βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))) β (((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
46 | 45 | 3impia 1118 |
. . . . . . . . . . . 12
β’ ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β βπ β
(0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
47 | 46 | impcom 409 |
. . . . . . . . . . 11
β’ ((((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) β βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}) |
48 | 5, 6, 47 | 3jca 1129 |
. . . . . . . . . 10
β’ ((((πΊ β V β§ πΉ β V β§ π β V) β§ πΊ β UPGraph) β§ (πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ))))) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
49 | 48 | exp31 421 |
. . . . . . . . 9
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΊ β UPGraph β ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})))) |
50 | 49 | com23 86 |
. . . . . . . 8
β’ ((πΊ β V β§ πΉ β V β§ π β V) β ((πΉ β Word dom
(iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β
(0..^(β―βπΉ))if-((πβπ) = (πβ(π + 1)), ((iEdgβπΊ)β(πΉβπ)) = {(πβπ)}, {(πβπ), (πβ(π + 1))} β ((iEdgβπΊ)β(πΉβπ)))) β (πΊ β UPGraph β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})))) |
51 | 4, 50 | sylbid 239 |
. . . . . . 7
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(WalksβπΊ)π β (πΊ β UPGraph β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})))) |
52 | 51 | impd 412 |
. . . . . 6
β’ ((πΊ β V β§ πΉ β V β§ π β V) β ((πΉ(WalksβπΊ)π β§ πΊ β UPGraph) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
53 | 52 | impcom 409 |
. . . . 5
β’ (((πΉ(WalksβπΊ)π β§ πΊ β UPGraph) β§ (πΊ β V β§ πΉ β V β§ π β V)) β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))})) |
54 | 2, 3 | isupwlk 46124 |
. . . . . 6
β’ ((πΊ β V β§ πΉ β V β§ π β V) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
55 | 54 | adantl 483 |
. . . . 5
β’ (((πΉ(WalksβπΊ)π β§ πΊ β UPGraph) β§ (πΊ β V β§ πΉ β V β§ π β V)) β (πΉ(UPWalksβπΊ)π β (πΉ β Word dom (iEdgβπΊ) β§ π:(0...(β―βπΉ))βΆ(VtxβπΊ) β§ βπ β (0..^(β―βπΉ))((iEdgβπΊ)β(πΉβπ)) = {(πβπ), (πβ(π + 1))}))) |
56 | 53, 55 | mpbird 257 |
. . . 4
β’ (((πΉ(WalksβπΊ)π β§ πΊ β UPGraph) β§ (πΊ β V β§ πΉ β V β§ π β V)) β πΉ(UPWalksβπΊ)π) |
57 | 56 | exp31 421 |
. . 3
β’ (πΉ(WalksβπΊ)π β (πΊ β UPGraph β ((πΊ β V β§ πΉ β V β§ π β V) β πΉ(UPWalksβπΊ)π))) |
58 | 1, 57 | mpid 44 |
. 2
β’ (πΉ(WalksβπΊ)π β (πΊ β UPGraph β πΉ(UPWalksβπΊ)π)) |
59 | 58 | impcom 409 |
1
β’ ((πΊ β UPGraph β§ πΉ(WalksβπΊ)π) β πΉ(UPWalksβπΊ)π) |