Step | Hyp | Ref
| Expression |
1 | | 1nn0 11308 |
. . . . . . . . 9
|
2 | | iswwlksn 26730 |
. . . . . . . . 9
WWalksN WWalks |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
WWalksN WWalks |
4 | | rusgrnumwwlkl1.v |
. . . . . . . . . 10
Vtx |
5 | | eqid 2622 |
. . . . . . . . . 10
Edg Edg |
6 | 4, 5 | iswwlks 26728 |
. . . . . . . . 9
WWalks Word ..^ Edg |
7 | 6 | anbi1i 731 |
. . . . . . . 8
WWalks
Word ..^ Edg |
8 | 3, 7 | bitri 264 |
. . . . . . 7
WWalksN Word ..^ Edg |
9 | 8 | a1i 11 |
. . . . . 6
RegUSGraph
WWalksN
Word ..^ Edg |
10 | 9 | anbi1d 741 |
. . . . 5
RegUSGraph
WWalksN
Word ..^ Edg |
11 | | 1p1e2 11134 |
. . . . . . . . . . 11
|
12 | 11 | eqeq2i 2634 |
. . . . . . . . . 10
|
13 | 12 | a1i 11 |
. . . . . . . . 9
RegUSGraph
|
14 | 13 | anbi2d 740 |
. . . . . . . 8
RegUSGraph
Word ..^ Edg Word ..^ Edg |
15 | | 3anass 1042 |
. . . . . . . . . . . 12
Word ..^ Edg
Word
..^ Edg |
16 | 15 | a1i 11 |
. . . . . . . . . . 11
RegUSGraph
Word ..^ Edg
Word
..^ Edg |
17 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
|
18 | | hash0 13158 |
. . . . . . . . . . . . . . . 16
|
19 | 17, 18 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
|
20 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . 17
|
21 | 20 | nesymi 2851 |
. . . . . . . . . . . . . . . 16
|
22 | | eqeq1 2626 |
. . . . . . . . . . . . . . . 16
|
23 | 21, 22 | mtbiri 317 |
. . . . . . . . . . . . . . 15
|
24 | 19, 23 | syl 17 |
. . . . . . . . . . . . . 14
|
25 | 24 | necon2ai 2823 |
. . . . . . . . . . . . 13
|
26 | 25 | adantl 482 |
. . . . . . . . . . . 12
RegUSGraph
|
27 | 26 | biantrurd 529 |
. . . . . . . . . . 11
RegUSGraph
Word
..^ Edg Word
..^ Edg |
28 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
|
29 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . 17
|
30 | 28, 29 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
|
31 | 30 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
..^ ..^ |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . 14
RegUSGraph
..^ ..^ |
33 | 32 | raleqdv 3144 |
. . . . . . . . . . . . 13
RegUSGraph
..^ Edg
..^ Edg |
34 | | fzo01 12550 |
. . . . . . . . . . . . . . 15
..^ |
35 | 34 | raleqi 3142 |
. . . . . . . . . . . . . 14
..^ Edg
Edg |
36 | | c0ex 10034 |
. . . . . . . . . . . . . . 15
|
37 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
38 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
39 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 38, 39 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
42 | 37, 41 | preq12d 4276 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
Edg
Edg |
44 | 36, 43 | ralsn 4222 |
. . . . . . . . . . . . . 14
Edg
Edg |
45 | 35, 44 | bitri 264 |
. . . . . . . . . . . . 13
..^ Edg
Edg |
46 | 33, 45 | syl6bb 276 |
. . . . . . . . . . . 12
RegUSGraph
..^ Edg
Edg |
47 | 46 | anbi2d 740 |
. . . . . . . . . . 11
RegUSGraph
Word
..^ Edg Word Edg |
48 | 16, 27, 47 | 3bitr2d 296 |
. . . . . . . . . 10
RegUSGraph
Word ..^ Edg
Word Edg |
49 | 48 | ex 450 |
. . . . . . . . 9
RegUSGraph
Word ..^ Edg
Word Edg |
50 | 49 | pm5.32rd 672 |
. . . . . . . 8
RegUSGraph
Word ..^ Edg Word Edg |
51 | 14, 50 | bitrd 268 |
. . . . . . 7
RegUSGraph
Word ..^ Edg Word Edg |
52 | 51 | anbi1d 741 |
. . . . . 6
RegUSGraph
Word ..^ Edg Word Edg |
53 | | anass 681 |
. . . . . 6
Word Edg Word Edg |
54 | 52, 53 | syl6bb 276 |
. . . . 5
RegUSGraph
Word ..^ Edg Word Edg |
55 | | anass 681 |
. . . . . . 7
Word Edg Word Edg |
56 | | ancom 466 |
. . . . . . . . 9
Edg
Edg |
57 | | df-3an 1039 |
. . . . . . . . 9
Edg
Edg |
58 | 56, 57 | bitr4i 267 |
. . . . . . . 8
Edg
Edg |
59 | 58 | anbi2i 730 |
. . . . . . 7
Word Edg Word Edg |
60 | 55, 59 | bitri 264 |
. . . . . 6
Word Edg Word Edg |
61 | 60 | a1i 11 |
. . . . 5
RegUSGraph
Word Edg
Word
Edg |
62 | 10, 54, 61 | 3bitrd 294 |
. . . 4
RegUSGraph
WWalksN
Word
Edg |
63 | 62 | rabbidva2 3186 |
. . 3
RegUSGraph
WWalksN Word
Edg |
64 | 63 | fveq2d 6195 |
. 2
RegUSGraph
WWalksN Word
Edg |
65 | 4 | rusgrnumwrdl2 26482 |
. 2
RegUSGraph
Word
Edg |
66 | 64, 65 | eqtrd 2656 |
1
RegUSGraph
WWalksN |