Step | Hyp | Ref
| Expression |
1 | | wlkv 26508 |
. . 3
Walks
|
2 | | eqid 2622 |
. . . . . . . . 9
Vtx Vtx |
3 | | eqid 2622 |
. . . . . . . . 9
iEdg iEdg |
4 | 2, 3 | iswlk 26506 |
. . . . . . . 8
Walks Word iEdg Vtx
..^if- iEdg iEdg |
5 | | simpr1 1067 |
. . . . . . . . . . 11
UPGraph Word iEdg Vtx
..^if- iEdg iEdg Word iEdg |
6 | | simpr2 1068 |
. . . . . . . . . . 11
UPGraph Word iEdg Vtx
..^if- iEdg iEdg Vtx |
7 | | df-ifp 1013 |
. . . . . . . . . . . . . . . . 17
if- iEdg
iEdg
iEdg iEdg |
8 | | dfsn2 4190 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
9 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
10 | 8, 9 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
|
11 | 10 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg
iEdg |
12 | 11 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
iEdg iEdg |
13 | 12 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
iEdg Word iEdg Vtx
UPGraph
..^ iEdg |
14 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
UPGraph
UPGraph |
15 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word iEdg Vtx
Word iEdg |
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Edg Edg |
17 | 3, 16 | upgredginwlk 26532 |
. . . . . . . . . . . . . . . . . . . . . . 23
UPGraph
Word iEdg
..^ iEdg Edg |
18 | 14, 15, 17 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . 22
Word iEdg Vtx
UPGraph
..^ iEdg Edg |
19 | 18 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
Word iEdg Vtx
UPGraph
..^ iEdg Edg |
20 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word iEdg Vtx
UPGraph
UPGraph |
21 | 20 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word iEdg Vtx
UPGraph
..^
UPGraph |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
iEdg
Vtx
UPGraph ..^ iEdg Edg
UPGraph |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg
UPGraph |
24 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg iEdg Edg |
25 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg
iEdg |
26 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
27 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
28 | | fvexd 6203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
29 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
30 | 27, 28, 29 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
31 | 26, 30 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg |
33 | 32 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg |
34 | 2, 16 | upgredgpr 26037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
UPGraph iEdg Edg iEdg iEdg |
35 | 23, 24, 25, 33, 34 | syl31anc 1329 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg iEdg |
36 | 35 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg iEdg |
37 | 36 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . 21
Word iEdg Vtx
UPGraph
..^ iEdg Edg iEdg iEdg |
38 | 19, 37 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
Word iEdg Vtx
UPGraph
..^ iEdg iEdg |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
iEdg Word iEdg Vtx
UPGraph
..^ iEdg |
40 | 13, 39 | jaoi 394 |
. . . . . . . . . . . . . . . . . 18
iEdg iEdg Word iEdg Vtx
UPGraph
..^ iEdg |
41 | 40 | com12 32 |
. . . . . . . . . . . . . . . . 17
Word iEdg Vtx
UPGraph
..^ iEdg iEdg iEdg |
42 | 7, 41 | syl5bi 232 |
. . . . . . . . . . . . . . . 16
Word iEdg Vtx
UPGraph
..^ if- iEdg iEdg iEdg |
43 | 42 | ralimdva 2962 |
. . . . . . . . . . . . . . 15
Word iEdg Vtx
UPGraph
..^if- iEdg iEdg ..^iEdg |
44 | 43 | ex 450 |
. . . . . . . . . . . . . 14
Word iEdg Vtx UPGraph
..^if- iEdg iEdg ..^iEdg |
45 | 44 | com23 86 |
. . . . . . . . . . . . 13
Word iEdg Vtx ..^if- iEdg
iEdg
UPGraph ..^iEdg |
46 | 45 | 3impia 1261 |
. . . . . . . . . . . 12
Word iEdg Vtx
..^if- iEdg iEdg UPGraph
..^iEdg |
47 | 46 | impcom 446 |
. . . . . . . . . . 11
UPGraph Word iEdg Vtx
..^if- iEdg iEdg ..^iEdg |
48 | 5, 6, 47 | 3jca 1242 |
. . . . . . . . . 10
UPGraph Word iEdg Vtx
..^if- iEdg iEdg Word iEdg Vtx
..^iEdg |
49 | 48 | exp31 630 |
. . . . . . . . 9
UPGraph Word iEdg Vtx
..^if- iEdg iEdg Word iEdg Vtx
..^iEdg |
50 | 49 | com23 86 |
. . . . . . . 8
Word iEdg Vtx
..^if- iEdg iEdg UPGraph Word iEdg Vtx
..^iEdg |
51 | 4, 50 | sylbid 230 |
. . . . . . 7
Walks UPGraph Word iEdg Vtx
..^iEdg |
52 | 51 | impd 447 |
. . . . . 6
Walks
UPGraph
Word iEdg Vtx
..^iEdg |
53 | 52 | impcom 446 |
. . . . 5
Walks
UPGraph
Word iEdg Vtx
..^iEdg |
54 | 2, 3 | isupwlk 41717 |
. . . . . 6
UPWalks Word iEdg Vtx
..^iEdg |
55 | 54 | adantl 482 |
. . . . 5
Walks
UPGraph
UPWalks
Word iEdg
Vtx ..^iEdg |
56 | 53, 55 | mpbird 247 |
. . . 4
Walks
UPGraph
UPWalks |
57 | 56 | exp31 630 |
. . 3
Walks UPGraph
UPWalks |
58 | 1, 57 | mpid 44 |
. 2
Walks UPGraph UPWalks |
59 | 58 | impcom 446 |
1
UPGraph
Walks UPWalks |