Step | Hyp | Ref
| Expression |
1 | | extwwlkfab.v |
. . 3
Vtx |
2 | | extwwlkfab.f |
. . 3
ClWWalksN |
3 | | extwwlkfab.c |
. . 3
ClWWalksN |
4 | | numclwwlk.t |
. . 3
substr
|
5 | 1, 2, 3, 4 | numclwlk1lem2f 27225 |
. 2
USGraph
NeighbVtx
|
6 | 1, 2, 3, 4 | numclwlk1lem2fv 27226 |
. . . . . 6
substr
|
7 | 6 | ad2antrl 764 |
. . . . 5
USGraph
substr |
8 | 1, 2, 3, 4 | numclwlk1lem2fv 27226 |
. . . . . 6
substr
|
9 | 8 | ad2antll 765 |
. . . . 5
USGraph
substr |
10 | 7, 9 | eqeq12d 2637 |
. . . 4
USGraph
substr
substr |
11 | | ovex 6678 |
. . . . . 6
substr |
12 | | fvex 6201 |
. . . . . 6
|
13 | 11, 12 | opth 4945 |
. . . . 5
substr
substr substr substr
|
14 | | uzuzle23 11729 |
. . . . . . . . . 10
|
15 | 3 | numclwwlkovgel 27221 |
. . . . . . . . . 10
ClWWalksN
|
16 | 14, 15 | sylan2 491 |
. . . . . . . . 9
ClWWalksN
|
17 | 1 | clwwlknbp 26885 |
. . . . . . . . . . 11
ClWWalksN Word |
18 | 17 | 3ad2ant1 1082 |
. . . . . . . . . 10
ClWWalksN
Word |
19 | | 3simpc 1060 |
. . . . . . . . . 10
ClWWalksN
|
20 | 18, 19 | jca 554 |
. . . . . . . . 9
ClWWalksN
Word |
21 | 16, 20 | syl6bi 243 |
. . . . . . . 8
Word
|
22 | 21 | 3adant1 1079 |
. . . . . . 7
USGraph
Word
|
23 | 3 | numclwwlkovgel 27221 |
. . . . . . . . . 10
ClWWalksN
|
24 | 14, 23 | sylan2 491 |
. . . . . . . . 9
ClWWalksN
|
25 | 1 | clwwlknbp 26885 |
. . . . . . . . . . 11
ClWWalksN Word |
26 | 25 | 3ad2ant1 1082 |
. . . . . . . . . 10
ClWWalksN
Word |
27 | | 3simpc 1060 |
. . . . . . . . . 10
ClWWalksN
|
28 | 26, 27 | jca 554 |
. . . . . . . . 9
ClWWalksN
Word |
29 | 24, 28 | syl6bi 243 |
. . . . . . . 8
Word
|
30 | 29 | 3adant1 1079 |
. . . . . . 7
USGraph
Word
|
31 | | simpll 790 |
. . . . . . . . . . 11
Word
Word |
32 | 31 | ad2antrl 764 |
. . . . . . . . . 10
USGraph
Word Word
Word |
33 | | simprll 802 |
. . . . . . . . . . 11
Word Word Word |
34 | 33 | adantl 482 |
. . . . . . . . . 10
USGraph
Word Word
Word |
35 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | eqcoms 2630 |
. . . . . . . . . . . . . . . 16
|
37 | | eluz2 11693 |
. . . . . . . . . . . . . . . . 17
|
38 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . 21
|
39 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . . 22
|
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . 21
|
42 | 38, 40, 41 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | | 1lt3 11196 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . . . 21
|
45 | 44 | expd 452 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 42, 43, 45 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | imp 445 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | 3adant1 1079 |
. . . . . . . . . . . . . . . . 17
|
49 | 37, 48 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
50 | 36, 49 | syl6bi 243 |
. . . . . . . . . . . . . . 15
|
51 | 50 | com12 32 |
. . . . . . . . . . . . . 14
|
52 | 51 | 3ad2ant3 1084 |
. . . . . . . . . . . . 13
USGraph
|
53 | 52 | com12 32 |
. . . . . . . . . . . 12
USGraph
|
54 | 53 | ad3antlr 767 |
. . . . . . . . . . 11
Word Word USGraph
|
55 | 54 | impcom 446 |
. . . . . . . . . 10
USGraph
Word Word
|
56 | | 2swrd2eqwrdeq 13696 |
. . . . . . . . . 10
Word
Word
substr
substr
lastS lastS |
57 | 32, 34, 55, 56 | syl3anc 1326 |
. . . . . . . . 9
USGraph
Word Word
substr substr
lastS lastS |
58 | | eqtr3 2643 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | expcom 451 |
. . . . . . . . . . . . . . 15
|
60 | 59 | ad2antlr 763 |
. . . . . . . . . . . . . 14
Word |
61 | 60 | com12 32 |
. . . . . . . . . . . . 13
Word |
62 | 61 | ad2antlr 763 |
. . . . . . . . . . . 12
Word Word
|
63 | 62 | imp 445 |
. . . . . . . . . . 11
Word Word |
64 | 63 | adantl 482 |
. . . . . . . . . 10
USGraph
Word Word
|
65 | 64 | biantrurd 529 |
. . . . . . . . 9
USGraph
Word Word
substr
substr
lastS lastS
substr
substr
lastS lastS |
66 | | 3anan12 1051 |
. . . . . . . . . . 11
substr substr
lastS lastS
substr substr
lastS lastS |
67 | 66 | a1i 11 |
. . . . . . . . . 10
USGraph
Word Word
substr
substr
lastS lastS
substr substr
lastS lastS |
68 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . 19
|
69 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
70 | 69 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . 22
|
71 | 70 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
|
72 | 71 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 72 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 68, 73 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | com12 32 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . 15
Word |
78 | 77 | imp 445 |
. . . . . . . . . . . . . 14
Word |
79 | 78 | adantr 481 |
. . . . . . . . . . . . 13
Word Word |
80 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
82 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | eqcoms 2630 |
. . . . . . . . . . . . . . . . 17
|
84 | 83 | biimpac 503 |
. . . . . . . . . . . . . . . 16
|
85 | 84 | adantl 482 |
. . . . . . . . . . . . . . 15
Word
|
86 | 81, 85 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
Word |
87 | 86 | ad4ant24 1298 |
. . . . . . . . . . . . 13
Word Word |
88 | 79, 87 | eqtr4d 2659 |
. . . . . . . . . . . 12
Word Word |
89 | 88 | adantl 482 |
. . . . . . . . . . 11
USGraph
Word Word
|
90 | 89 | biantrurd 529 |
. . . . . . . . . 10
USGraph
Word Word
substr
substr
lastS lastS
substr substr
lastS lastS |
91 | 80 | opeq2d 4409 |
. . . . . . . . . . . . . . 15
|
92 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . 14
substr substr |
93 | 91 | oveq2d 6666 |
. . . . . . . . . . . . . 14
substr substr |
94 | 92, 93 | eqeq12d 2637 |
. . . . . . . . . . . . 13
substr
substr
substr substr
|
95 | 94 | ad3antlr 767 |
. . . . . . . . . . . 12
Word Word substr substr substr substr
|
96 | 95 | adantl 482 |
. . . . . . . . . . 11
USGraph
Word Word
substr
substr
substr substr
|
97 | | lsw 13351 |
. . . . . . . . . . . . . . 15
Word lastS |
98 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
99 | 98 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
100 | 97, 99 | sylan9eq 2676 |
. . . . . . . . . . . . . 14
Word lastS
|
101 | 100 | adantr 481 |
. . . . . . . . . . . . 13
Word lastS
|
102 | | lsw 13351 |
. . . . . . . . . . . . . . . 16
Word lastS |
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . 15
Word lastS |
104 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 104 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . 18
|
106 | 105 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
lastS lastS |
108 | 107 | adantl 482 |
. . . . . . . . . . . . . . 15
Word lastS
lastS |
109 | 103, 108 | mpbird 247 |
. . . . . . . . . . . . . 14
Word lastS
|
110 | 109 | adantr 481 |
. . . . . . . . . . . . 13
Word lastS
|
111 | 101, 110 | eqeqan12d 2638 |
. . . . . . . . . . . 12
Word Word lastS lastS
|
112 | 111 | adantl 482 |
. . . . . . . . . . 11
USGraph
Word Word
lastS lastS
|
113 | 96, 112 | anbi12d 747 |
. . . . . . . . . 10
USGraph
Word Word
substr
substr
lastS lastS
substr
substr
|
114 | 67, 90, 113 | 3bitr2d 296 |
. . . . . . . . 9
USGraph
Word Word
substr
substr
lastS lastS
substr
substr
|
115 | 57, 65, 114 | 3bitr2d 296 |
. . . . . . . 8
USGraph
Word Word
substr substr
|
116 | 115 | exbiri 652 |
. . . . . . 7
USGraph
Word Word substr
substr
|
117 | 22, 30, 116 | syl2and 500 |
. . . . . 6
USGraph
substr substr
|
118 | 117 | imp 445 |
. . . . 5
USGraph
substr substr
|
119 | 13, 118 | syl5bi 232 |
. . . 4
USGraph
substr
substr |
120 | 10, 119 | sylbid 230 |
. . 3
USGraph
|
121 | 120 | ralrimivva 2971 |
. 2
USGraph
|
122 | | dff13 6512 |
. 2
NeighbVtx NeighbVtx
|
123 | 5, 121, 122 | sylanbrc 698 |
1
USGraph
NeighbVtx
|