Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
Vtx Vtx |
2 | 1 | wwlkbp 26732 |
. . 3
WWalks
Word Vtx |
3 | | eqid 2622 |
. . . . 5
Edg Edg |
4 | 1, 3 | iswwlks 26728 |
. . . 4
WWalks Word Vtx
..^ Edg |
5 | | ovex 6678 |
. . . . . . . . . . . . . . 15
..^ |
6 | | mptexg 6484 |
. . . . . . . . . . . . . . 15
..^ ..^ iEdg |
7 | 5, 6 | mp1i 13 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx
USPGraph
..^ iEdg |
8 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx
USPGraph
USPGraph |
9 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx
USPGraph
Word Vtx |
10 | | hashge1 13178 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx |
11 | 10 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
12 | 11 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx
USPGraph
|
13 | 8, 9, 12 | 3jca 1242 |
. . . . . . . . . . . . . . . . 17
Word Vtx
Word Vtx
USPGraph
USPGraph Word Vtx |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . . . 16
Word Vtx
Word Vtx USPGraph ..^ iEdg USPGraph Word Vtx
|
15 | | edgval 25941 |
. . . . . . . . . . . . . . . . . . . 20
Edg iEdg |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
Word Vtx USPGraph ..^ iEdg Edg iEdg |
17 | 16 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx USPGraph ..^ iEdg Edg
iEdg |
18 | 17 | ralbidv 2986 |
. . . . . . . . . . . . . . . . 17
Word Vtx
Word Vtx USPGraph ..^ iEdg ..^ Edg
..^ iEdg |
19 | 18 | biimpd 219 |
. . . . . . . . . . . . . . . 16
Word Vtx
Word Vtx USPGraph ..^ iEdg ..^ Edg ..^ iEdg |
20 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
..^ iEdg ..^ iEdg |
21 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg |
22 | 20, 21 | wlkiswwlks2lem6 26760 |
. . . . . . . . . . . . . . . 16
USPGraph
Word Vtx
..^ iEdg ..^ iEdg Word iEdg ..^ iEdg Vtx ..^ ..^ iEdg iEdg ..^ iEdg |
23 | 14, 19, 22 | sylsyld 61 |
. . . . . . . . . . . . . . 15
Word Vtx
Word Vtx USPGraph ..^ iEdg ..^ Edg ..^ iEdg Word iEdg ..^ iEdg Vtx ..^ ..^ iEdg iEdg ..^ iEdg |
24 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
..^ iEdg Word
iEdg
..^ iEdg Word iEdg |
25 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
..^ iEdg ..^ iEdg |
26 | 25 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
..^ iEdg ..^ iEdg |
27 | 26 | feq2d 6031 |
. . . . . . . . . . . . . . . . . 18
..^ iEdg Vtx
..^ iEdg Vtx |
28 | 25 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
..^ iEdg ..^ ..^ ..^ iEdg |
29 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . 21
..^ iEdg ..^ iEdg |
30 | 29 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
..^ iEdg iEdg iEdg ..^ iEdg |
31 | 30 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . 19
..^ iEdg iEdg iEdg ..^ iEdg |
32 | 28, 31 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . 18
..^ iEdg
..^iEdg
..^ ..^ iEdg iEdg ..^ iEdg |
33 | 24, 27, 32 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . 17
..^ iEdg Word iEdg Vtx
..^iEdg ..^ iEdg Word iEdg ..^ iEdg Vtx ..^ ..^ iEdg iEdg ..^ iEdg |
34 | 33 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
..^ iEdg ..^ Edg Word
iEdg Vtx
..^iEdg ..^ Edg ..^ iEdg Word iEdg ..^ iEdg Vtx ..^ ..^ iEdg iEdg ..^ iEdg |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . 15
Word Vtx
Word Vtx USPGraph ..^ iEdg ..^ Edg Word
iEdg Vtx
..^iEdg ..^ Edg ..^ iEdg Word iEdg ..^ iEdg Vtx ..^ ..^ iEdg iEdg ..^ iEdg |
36 | 23, 35 | mpbird 247 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx USPGraph ..^ iEdg ..^ Edg Word
iEdg Vtx
..^iEdg |
37 | 7, 36 | spcimedv 3292 |
. . . . . . . . . . . . 13
Word Vtx
Word Vtx
USPGraph
..^ Edg Word iEdg Vtx
..^iEdg |
38 | 37 | ex 450 |
. . . . . . . . . . . 12
Word Vtx
Word Vtx
USPGraph
..^ Edg Word iEdg Vtx
..^iEdg |
39 | 38 | com23 86 |
. . . . . . . . . . 11
Word Vtx
..^ Edg Word Vtx
USPGraph Word
iEdg
Vtx ..^iEdg |
40 | 39 | 3impia 1261 |
. . . . . . . . . 10
Word Vtx ..^ Edg
Word Vtx USPGraph
Word iEdg Vtx
..^iEdg |
41 | 40 | expd 452 |
. . . . . . . . 9
Word Vtx ..^ Edg Word Vtx
USPGraph Word
iEdg
Vtx ..^iEdg |
42 | 41 | impcom 446 |
. . . . . . . 8
Word Vtx
Word Vtx ..^ Edg
USPGraph Word
iEdg
Vtx ..^iEdg |
43 | 42 | imp 445 |
. . . . . . 7
Word Vtx Word Vtx
..^ Edg USPGraph Word
iEdg
Vtx ..^iEdg |
44 | | uspgrupgr 26071 |
. . . . . . . . . 10
USPGraph UPGraph |
45 | 1, 21 | upgriswlk 26537 |
. . . . . . . . . 10
UPGraph Walks
Word iEdg
Vtx ..^iEdg |
46 | 44, 45 | syl 17 |
. . . . . . . . 9
USPGraph Walks
Word iEdg
Vtx ..^iEdg |
47 | 46 | adantl 482 |
. . . . . . . 8
Word Vtx Word Vtx
..^ Edg USPGraph Walks
Word iEdg
Vtx ..^iEdg |
48 | 47 | exbidv 1850 |
. . . . . . 7
Word Vtx Word Vtx
..^ Edg USPGraph Walks
Word iEdg Vtx
..^iEdg |
49 | 43, 48 | mpbird 247 |
. . . . . 6
Word Vtx Word Vtx
..^ Edg USPGraph Walks |
50 | 49 | ex 450 |
. . . . 5
Word Vtx
Word Vtx ..^ Edg
USPGraph Walks |
51 | 50 | ex 450 |
. . . 4
Word Vtx Word Vtx ..^ Edg USPGraph Walks |
52 | 4, 51 | syl5bi 232 |
. . 3
Word Vtx
WWalks
USPGraph Walks |
53 | 2, 52 | mpcom 38 |
. 2
WWalks
USPGraph Walks |
54 | 53 | com12 32 |
1
USPGraph WWalks Walks |