Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
Vtx Vtx |
2 | | eqid 2622 |
. . 3
Edg Edg |
3 | 1, 2 | iswwlks 26728 |
. 2
WWalks Word Vtx
..^ Edg |
4 | | edgval 25941 |
. . . . . . . . . . . . 13
Edg iEdg |
5 | 4 | eleq2i 2693 |
. . . . . . . . . . . 12
Edg iEdg |
6 | | upgruhgr 25997 |
. . . . . . . . . . . . . . 15
UPGraph UHGraph |
7 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
iEdg iEdg |
8 | 7 | uhgrfun 25961 |
. . . . . . . . . . . . . . 15
UHGraph
iEdg |
9 | 6, 8 | syl 17 |
. . . . . . . . . . . . . 14
UPGraph
iEdg |
10 | 9 | adantl 482 |
. . . . . . . . . . . . 13
Word Vtx
UPGraph
iEdg |
11 | | elrnrexdm 6363 |
. . . . . . . . . . . . . 14
iEdg iEdg
iEdg iEdg |
12 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
iEdg iEdg |
13 | 12 | rexbii 3041 |
. . . . . . . . . . . . . 14
iEdgiEdg
iEdg iEdg |
14 | 11, 13 | syl6ibr 242 |
. . . . . . . . . . . . 13
iEdg iEdg
iEdgiEdg |
15 | 10, 14 | syl 17 |
. . . . . . . . . . . 12
Word Vtx
UPGraph iEdg iEdgiEdg |
16 | 5, 15 | syl5bi 232 |
. . . . . . . . . . 11
Word Vtx
UPGraph Edg
iEdgiEdg |
17 | 16 | ralimdv 2963 |
. . . . . . . . . 10
Word Vtx
UPGraph ..^ Edg ..^ iEdgiEdg |
18 | 17 | ex 450 |
. . . . . . . . 9
Word Vtx
UPGraph ..^ Edg ..^ iEdgiEdg |
19 | 18 | com23 86 |
. . . . . . . 8
Word Vtx
..^ Edg UPGraph ..^ iEdgiEdg |
20 | 19 | 3impia 1261 |
. . . . . . 7
Word Vtx ..^ Edg UPGraph ..^ iEdgiEdg |
21 | 20 | impcom 446 |
. . . . . 6
UPGraph
Word Vtx ..^ Edg
..^ iEdgiEdg |
22 | | ovex 6678 |
. . . . . . 7
..^ |
23 | | fvex 6201 |
. . . . . . . 8
iEdg |
24 | 23 | dmex 7099 |
. . . . . . 7
iEdg |
25 | | fveq2 6191 |
. . . . . . . 8
iEdg iEdg |
26 | 25 | eqeq1d 2624 |
. . . . . . 7
iEdg iEdg |
27 | 22, 24, 26 | ac6 9302 |
. . . . . 6
..^ iEdgiEdg
..^ iEdg
..^ iEdg |
28 | 21, 27 | syl 17 |
. . . . 5
UPGraph
Word Vtx ..^ Edg
..^ iEdg
..^ iEdg |
29 | | iswrdi 13309 |
. . . . . . . . . 10
..^
iEdg
Word iEdg |
30 | 29 | adantr 481 |
. . . . . . . . 9
..^
iEdg
..^ iEdg Word iEdg |
31 | 30 | adantl 482 |
. . . . . . . 8
UPGraph Word Vtx ..^ Edg ..^
iEdg
..^ iEdg Word
iEdg |
32 | | wrdfin 13323 |
. . . . . . . . . . . . . . . 16
Word Vtx
|
33 | | hashnncl 13157 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | bicomd 213 |
. . . . . . . . . . . . . . . 16
|
35 | 32, 34 | syl 17 |
. . . . . . . . . . . . . . 15
Word Vtx
|
36 | 35 | biimpac 503 |
. . . . . . . . . . . . . 14
Word Vtx
|
37 | | wrdf 13310 |
. . . . . . . . . . . . . . . 16
Word Vtx
..^Vtx |
38 | | nnz 11399 |
. . . . . . . . . . . . . . . . . . . . . 22
|
39 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
..^
iEdg ..^ |
42 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
43 | | fnfzo0hash 13234 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
iEdg |
44 | 42, 43 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
iEdg |
45 | 44 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
..^
iEdg |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . 20
..^
iEdg |
47 | 41, 46 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
..^
iEdg ..^ |
48 | 47 | feq2d 6031 |
. . . . . . . . . . . . . . . . . 18
..^
iEdg ..^Vtx Vtx |
49 | 48 | biimpcd 239 |
. . . . . . . . . . . . . . . . 17
..^Vtx
..^
iEdg Vtx |
50 | 49 | expd 452 |
. . . . . . . . . . . . . . . 16
..^Vtx
..^
iEdg
Vtx |
51 | 37, 50 | syl 17 |
. . . . . . . . . . . . . . 15
Word Vtx
..^
iEdg
Vtx |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . 14
Word Vtx
..^
iEdg
Vtx |
53 | 36, 52 | mpd 15 |
. . . . . . . . . . . . 13
Word Vtx
..^
iEdg
Vtx |
54 | 53 | 3adant3 1081 |
. . . . . . . . . . . 12
Word Vtx ..^ Edg ..^ iEdg
Vtx |
55 | 54 | adantl 482 |
. . . . . . . . . . 11
UPGraph
Word Vtx ..^ Edg
..^
iEdg
Vtx |
56 | 55 | com12 32 |
. . . . . . . . . 10
..^
iEdg
UPGraph Word Vtx ..^ Edg
Vtx |
57 | 56 | adantr 481 |
. . . . . . . . 9
..^
iEdg
..^ iEdg UPGraph Word Vtx ..^ Edg
Vtx |
58 | 57 | impcom 446 |
. . . . . . . 8
UPGraph Word Vtx ..^ Edg ..^
iEdg
..^ iEdg Vtx |
59 | | simpr 477 |
. . . . . . . . . 10
UPGraph Word Vtx ..^ Edg ..^ iEdg
..^ iEdg ..^ iEdg |
60 | 36, 44 | sylan 488 |
. . . . . . . . . . . . . . . . 17
Word Vtx
..^ iEdg |
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
Word Vtx
..^ iEdg ..^ ..^ |
62 | 61 | ex 450 |
. . . . . . . . . . . . . . 15
Word Vtx
..^
iEdg
..^ ..^ |
63 | 62 | 3adant3 1081 |
. . . . . . . . . . . . . 14
Word Vtx ..^ Edg ..^ iEdg
..^ ..^ |
64 | 63 | adantl 482 |
. . . . . . . . . . . . 13
UPGraph
Word Vtx ..^ Edg
..^
iEdg
..^ ..^ |
65 | 64 | imp 445 |
. . . . . . . . . . . 12
UPGraph Word Vtx ..^ Edg ..^ iEdg ..^ ..^ |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
UPGraph Word Vtx ..^ Edg ..^ iEdg
..^ iEdg ..^ ..^ |
67 | 66 | raleqdv 3144 |
. . . . . . . . . 10
UPGraph Word Vtx ..^ Edg ..^ iEdg
..^ iEdg ..^iEdg
..^ iEdg |
68 | 59, 67 | mpbird 247 |
. . . . . . . . 9
UPGraph Word Vtx ..^ Edg ..^ iEdg
..^ iEdg ..^iEdg |
69 | 68 | anasss 679 |
. . . . . . . 8
UPGraph Word Vtx ..^ Edg ..^
iEdg
..^ iEdg
..^iEdg |
70 | 31, 58, 69 | 3jca 1242 |
. . . . . . 7
UPGraph Word Vtx ..^ Edg ..^
iEdg
..^ iEdg Word iEdg Vtx
..^iEdg |
71 | 70 | ex 450 |
. . . . . 6
UPGraph
Word Vtx ..^ Edg
..^
iEdg
..^ iEdg Word
iEdg Vtx
..^iEdg |
72 | 71 | eximdv 1846 |
. . . . 5
UPGraph
Word Vtx ..^ Edg
..^ iEdg
..^ iEdg Word iEdg Vtx
..^iEdg |
73 | 28, 72 | mpd 15 |
. . . 4
UPGraph
Word Vtx ..^ Edg
Word iEdg Vtx
..^iEdg |
74 | 1, 7 | upgriswlk 26537 |
. . . . . 6
UPGraph Walks
Word iEdg
Vtx ..^iEdg |
75 | 74 | adantr 481 |
. . . . 5
UPGraph
Word Vtx ..^ Edg
Walks Word iEdg Vtx
..^iEdg |
76 | 75 | exbidv 1850 |
. . . 4
UPGraph
Word Vtx ..^ Edg
Walks
Word iEdg Vtx
..^iEdg |
77 | 73, 76 | mpbird 247 |
. . 3
UPGraph
Word Vtx ..^ Edg
Walks |
78 | 77 | ex 450 |
. 2
UPGraph Word Vtx ..^ Edg Walks |
79 | 3, 78 | syl5bi 232 |
1
UPGraph WWalks Walks |