Step | Hyp | Ref
| Expression |
1 | | crctprop 26687 |
. . 3
Circuits Trails |
2 | | istrl 26593 |
. . . . . . 7
Trails Walks |
3 | | uspgrupgr 26071 |
. . . . . . . . 9
USPGraph UPGraph |
4 | | eqid 2622 |
. . . . . . . . . . . . 13
Vtx Vtx |
5 | | eqid 2622 |
. . . . . . . . . . . . 13
iEdg iEdg |
6 | 4, 5 | upgriswlk 26537 |
. . . . . . . . . . . 12
UPGraph Walks
Word iEdg
Vtx ..^iEdg |
7 | | preq2 4269 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
8 | | prcom 4267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
9 | 7, 8 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
10 | 9 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
11 | 10 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg
iEdg |
12 | 11 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg iEdg iEdg |
13 | 12 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
USPGraph Word iEdg
iEdg iEdg iEdg iEdg |
14 | | eqtr3 2643 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg
iEdg iEdg |
15 | 4, 5 | uspgrf 26049 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
USPGraph iEdg iEdg Vtx |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
USPGraph iEdg iEdg Vtx
|
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
USPGraph iEdg iEdg Vtx |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
USPGraph Word iEdg iEdg iEdg Vtx |
19 | | df-f1 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ iEdg ..^ iEdg |
20 | 19 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
iEdg
..^ iEdg |
21 | | wrdf 13310 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word
iEdg
..^ iEdg |
22 | 20, 21 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
iEdg
..^ iEdg |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
USPGraph
Word iEdg ..^ iEdg |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
USPGraph Word iEdg ..^ iEdg |
25 | 24 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
USPGraph Word iEdg ..^ iEdg |
26 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
27 | | lbfzo0 12507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ |
28 | 26, 27 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
29 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
30 | | 1lt2 11194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
31 | | elfzo0 12508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
32 | 29, 26, 30, 31 | mpbir3an 1244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
33 | 28, 32 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ ..^ |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^ ..^ |
35 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
..^ |
36 | 34 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^
..^ |
37 | 35, 36 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ ..^ ..^
..^ |
38 | 33, 37 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ ..^ |
39 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
USPGraph Word iEdg ..^
..^ |
40 | | f1cofveqaeq 6515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg iEdg Vtx ..^ iEdg ..^ ..^
iEdg iEdg |
41 | 18, 25, 39, 40 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . . 24
USPGraph Word iEdg iEdg iEdg
|
42 | | 0ne1 11088 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
43 | | eqneqall 2805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | 41, 42, 43 | syl6mpi 67 |
. . . . . . . . . . . . . . . . . . . . . . 23
USPGraph Word iEdg iEdg iEdg
|
45 | 44 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . 22
USPGraph Word iEdg
iEdg iEdg |
46 | 14, 45 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
USPGraph Word iEdg
iEdg iEdg
|
47 | 13, 46 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . 20
USPGraph Word iEdg
iEdg iEdg
|
48 | 47 | expimpd 629 |
. . . . . . . . . . . . . . . . . . 19
USPGraph
Word iEdg iEdg iEdg |
49 | 48 | ex 450 |
. . . . . . . . . . . . . . . . . 18
USPGraph Word
iEdg
iEdg iEdg
|
50 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
USPGraph Word
iEdg
iEdg iEdg
|
51 | 49, 50 | pm2.61ine 2877 |
. . . . . . . . . . . . . . . . 17
USPGraph Word
iEdg
iEdg iEdg
|
52 | | fzo0to2pr 12553 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
53 | 34, 52 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
54 | 53 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . 21
..^iEdg
iEdg |
55 | | 2wlklem 26563 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg iEdg iEdg |
56 | 54, 55 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . 20
..^iEdg
iEdg iEdg |
57 | 56 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . 19
Word iEdg ..^iEdg Word iEdg iEdg iEdg |
58 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
59 | 58 | neeq2d 2854 |
. . . . . . . . . . . . . . . . . . 19
|
60 | 57, 59 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
Word iEdg ..^iEdg
Word iEdg iEdg iEdg |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . . 17
USPGraph Word iEdg
..^iEdg
Word iEdg iEdg iEdg |
62 | 51, 61 | mpbird 247 |
. . . . . . . . . . . . . . . 16
USPGraph Word
iEdg
..^iEdg
|
63 | 62 | ex 450 |
. . . . . . . . . . . . . . 15
USPGraph Word iEdg ..^iEdg |
64 | 63 | com13 88 |
. . . . . . . . . . . . . 14
Word iEdg
..^iEdg
USPGraph |
65 | 64 | expd 452 |
. . . . . . . . . . . . 13
Word iEdg
..^iEdg USPGraph |
66 | 65 | 3adant2 1080 |
. . . . . . . . . . . 12
Word iEdg Vtx
..^iEdg USPGraph |
67 | 6, 66 | syl6bi 243 |
. . . . . . . . . . 11
UPGraph Walks
USPGraph |
68 | 67 | impd 447 |
. . . . . . . . . 10
UPGraph Walks
USPGraph |
69 | 68 | com23 86 |
. . . . . . . . 9
UPGraph USPGraph Walks |
70 | 3, 69 | mpcom 38 |
. . . . . . . 8
USPGraph Walks
|
71 | 70 | com12 32 |
. . . . . . 7
Walks
USPGraph |
72 | 2, 71 | sylbi 207 |
. . . . . 6
Trails USPGraph |
73 | 72 | imp 445 |
. . . . 5
Trails USPGraph
|
74 | 73 | necon2d 2817 |
. . . 4
Trails USPGraph
|
75 | 74 | impancom 456 |
. . 3
Trails
USPGraph |
76 | 1, 75 | syl 17 |
. 2
Circuits USPGraph |
77 | 76 | impcom 446 |
1
USPGraph
Circuits |