Step | Hyp | Ref
| Expression |
1 | | wlkn0 26516 |
. 2
Walks |
2 | | eqid 2622 |
. . . 4
Vtx Vtx |
3 | | eqid 2622 |
. . . 4
iEdg iEdg |
4 | 2, 3 | upgriswlk 26537 |
. . 3
UPGraph Walks
Word iEdg
Vtx ..^iEdg |
5 | | simpr 477 |
. . . . . 6
UPGraph
Word iEdg Vtx
..^iEdg
|
6 | | ffz0iswrd 13332 |
. . . . . . . 8
Vtx Word Vtx |
7 | 6 | 3ad2ant2 1083 |
. . . . . . 7
Word iEdg Vtx
..^iEdg Word Vtx |
8 | 7 | ad2antlr 763 |
. . . . . 6
UPGraph
Word iEdg Vtx
..^iEdg
Word Vtx |
9 | | upgruhgr 25997 |
. . . . . . . . . . . . . . . . . 18
UPGraph UHGraph |
10 | 3 | uhgrfun 25961 |
. . . . . . . . . . . . . . . . . 18
UHGraph
iEdg |
11 | | funfn 5918 |
. . . . . . . . . . . . . . . . . . 19
iEdg iEdg iEdg |
12 | 11 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
iEdg iEdg iEdg |
13 | 9, 10, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
UPGraph iEdg iEdg |
14 | 13 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
Word iEdg Vtx
UPGraph ..^ iEdg iEdg |
15 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . . . . 17
Word iEdg ..^ iEdg |
16 | 15 | ad4ant14 1293 |
. . . . . . . . . . . . . . . 16
Word iEdg Vtx
UPGraph ..^ iEdg |
17 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . 16
iEdg iEdg
iEdg iEdg iEdg |
18 | 14, 16, 17 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Word iEdg Vtx
UPGraph ..^ iEdg iEdg |
19 | | edgval 25941 |
. . . . . . . . . . . . . . 15
Edg iEdg |
20 | 18, 19 | syl6eleqr 2712 |
. . . . . . . . . . . . . 14
Word iEdg Vtx
UPGraph ..^ iEdg Edg |
21 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
iEdg
Edg iEdg Edg |
22 | 21 | eqcoms 2630 |
. . . . . . . . . . . . . 14
iEdg Edg
iEdg Edg |
23 | 20, 22 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
Word iEdg Vtx
UPGraph ..^ iEdg Edg |
24 | 23 | ralimdva 2962 |
. . . . . . . . . . . 12
Word iEdg Vtx
UPGraph
..^iEdg ..^ Edg |
25 | 24 | ex 450 |
. . . . . . . . . . 11
Word iEdg Vtx UPGraph ..^iEdg ..^ Edg |
26 | 25 | com23 86 |
. . . . . . . . . 10
Word iEdg Vtx ..^iEdg UPGraph ..^ Edg |
27 | 26 | 3impia 1261 |
. . . . . . . . 9
Word iEdg Vtx
..^iEdg UPGraph ..^ Edg |
28 | 27 | impcom 446 |
. . . . . . . 8
UPGraph
Word iEdg Vtx
..^iEdg
..^ Edg |
29 | | lencl 13324 |
. . . . . . . . . . . . . 14
Word
iEdg
|
30 | | ffz0hash 13231 |
. . . . . . . . . . . . . . . 16
Vtx |
31 | 30 | ex 450 |
. . . . . . . . . . . . . . 15
Vtx |
32 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
33 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . 18
|
34 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . 18
|
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
36 | 32, 35 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | ex 450 |
. . . . . . . . . . . . . . 15
|
38 | 31, 37 | syld 47 |
. . . . . . . . . . . . . 14
Vtx |
39 | 29, 38 | syl 17 |
. . . . . . . . . . . . 13
Word
iEdg
Vtx |
40 | 39 | imp 445 |
. . . . . . . . . . . 12
Word iEdg Vtx |
41 | 40 | oveq2d 6666 |
. . . . . . . . . . 11
Word iEdg Vtx ..^ ..^ |
42 | 41 | raleqdv 3144 |
. . . . . . . . . 10
Word iEdg Vtx ..^ Edg
..^ Edg |
43 | 42 | 3adant3 1081 |
. . . . . . . . 9
Word iEdg Vtx
..^iEdg ..^ Edg
..^ Edg |
44 | 43 | adantl 482 |
. . . . . . . 8
UPGraph
Word iEdg Vtx
..^iEdg
..^ Edg
..^ Edg |
45 | 28, 44 | mpbird 247 |
. . . . . . 7
UPGraph
Word iEdg Vtx
..^iEdg
..^ Edg |
46 | 45 | adantr 481 |
. . . . . 6
UPGraph
Word iEdg Vtx
..^iEdg
..^ Edg |
47 | | eqid 2622 |
. . . . . . 7
Edg Edg |
48 | 2, 47 | iswwlks 26728 |
. . . . . 6
WWalks Word Vtx
..^ Edg |
49 | 5, 8, 46, 48 | syl3anbrc 1246 |
. . . . 5
UPGraph
Word iEdg Vtx
..^iEdg
WWalks |
50 | 49 | ex 450 |
. . . 4
UPGraph
Word iEdg Vtx
..^iEdg
WWalks |
51 | 50 | ex 450 |
. . 3
UPGraph Word
iEdg
Vtx ..^iEdg WWalks |
52 | 4, 51 | sylbid 230 |
. 2
UPGraph Walks WWalks |
53 | 1, 52 | mpdi 45 |
1
UPGraph Walks
WWalks |