Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.1 |
. . 3
|
2 | | clwlksfclwwlk.2 |
. . 3
|
3 | | clwlksfclwwlk.c |
. . 3
ClWalks |
4 | | clwlksfclwwlk.f |
. . 3
substr |
5 | 1, 2, 3, 4 | clwlksfclwwlk 26962 |
. 2
FinUSGraph
ClWWalksN
|
6 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
7 | 6 | clwwlknbp 26885 |
. . . . 5
ClWWalksN Word Vtx |
8 | 7 | adantl 482 |
. . . 4
FinUSGraph ClWWalksN
Word Vtx |
9 | | prmnn 15388 |
. . . . . . . . 9
|
10 | 9 | ad2antlr 763 |
. . . . . . . 8
FinUSGraph Word
Vtx
|
11 | | isclwwlksn 26882 |
. . . . . . . 8
ClWWalksN
ClWWalks |
12 | 10, 11 | syl 17 |
. . . . . . 7
FinUSGraph Word
Vtx
ClWWalksN
ClWWalks
|
13 | | fusgrusgr 26214 |
. . . . . . . . . . . . 13
FinUSGraph USGraph |
14 | | usgruspgr 26073 |
. . . . . . . . . . . . 13
USGraph USPGraph |
15 | 13, 14 | syl 17 |
. . . . . . . . . . . 12
FinUSGraph USPGraph |
16 | 15 | adantr 481 |
. . . . . . . . . . 11
FinUSGraph
USPGraph |
17 | 16 | adantr 481 |
. . . . . . . . . 10
FinUSGraph Word
Vtx
USPGraph |
18 | | simprl 794 |
. . . . . . . . . 10
FinUSGraph Word
Vtx
Word Vtx |
19 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
20 | | prmnn 15388 |
. . . . . . . . . . . . . . . 16
|
21 | 20 | nnge1d 11063 |
. . . . . . . . . . . . . . 15
|
22 | 19, 21 | syl6bir 244 |
. . . . . . . . . . . . . 14
|
23 | 22 | adantl 482 |
. . . . . . . . . . . . 13
Word Vtx
|
24 | 23 | com12 32 |
. . . . . . . . . . . 12
Word Vtx |
25 | 24 | adantl 482 |
. . . . . . . . . . 11
FinUSGraph
Word Vtx |
26 | 25 | imp 445 |
. . . . . . . . . 10
FinUSGraph Word
Vtx
|
27 | | eqid 2622 |
. . . . . . . . . . 11
iEdg iEdg |
28 | 6, 27 | clwlkclwwlk2 26904 |
. . . . . . . . . 10
USPGraph
Word Vtx
ClWalks ++
ClWWalks |
29 | 17, 18, 26, 28 | syl3anc 1326 |
. . . . . . . . 9
FinUSGraph Word
Vtx
ClWalks ++ ClWWalks |
30 | 29 | bicomd 213 |
. . . . . . . 8
FinUSGraph Word
Vtx
ClWWalks ClWalks ++ |
31 | 30 | anbi1d 741 |
. . . . . . 7
FinUSGraph Word
Vtx
ClWWalks
ClWalks ++ |
32 | 12, 31 | bitrd 268 |
. . . . . 6
FinUSGraph Word
Vtx
ClWWalksN
ClWalks ++ |
33 | | df-br 4654 |
. . . . . . . . 9
ClWalks ++
++ ClWalks |
34 | | simpl 473 |
. . . . . . . . . . . . 13
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks |
35 | 9 | nnge1d 11063 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 35 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
FinUSGraph Word
Vtx
|
37 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . 19
|
38 | 37 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
FinUSGraph Word
Vtx
|
39 | 36, 38 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
FinUSGraph Word
Vtx
|
40 | 18, 39 | jca 554 |
. . . . . . . . . . . . . . . 16
FinUSGraph Word
Vtx
Word Vtx
|
41 | | clwlkwlk 26671 |
. . . . . . . . . . . . . . . 16
++ ClWalks
++ Walks |
42 | | wlklenvclwlk 26551 |
. . . . . . . . . . . . . . . 16
Word Vtx ++ Walks |
43 | 40, 41, 42 | syl2im 40 |
. . . . . . . . . . . . . . 15
FinUSGraph Word
Vtx
++ ClWalks
|
44 | 43 | impcom 446 |
. . . . . . . . . . . . . 14
++ ClWalks
FinUSGraph
Word
Vtx
|
45 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
|
46 | | ovex 6678 |
. . . . . . . . . . . . . . . . . 18
++
|
47 | 45, 46 | op1st 7176 |
. . . . . . . . . . . . . . . . 17
++ |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . . 16
FinUSGraph Word
Vtx
++ |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
FinUSGraph Word
Vtx
++ |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
++ ClWalks
FinUSGraph
Word
Vtx
++ |
51 | | eqcom 2629 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
53 | 52 | ad2antll 765 |
. . . . . . . . . . . . . . 15
FinUSGraph Word
Vtx
|
54 | 53 | adantl 482 |
. . . . . . . . . . . . . 14
++ ClWalks
FinUSGraph
Word
Vtx
|
55 | 44, 50, 54 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
++ ClWalks
FinUSGraph
Word
Vtx
++ |
56 | 1 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | eqeq1i 2627 |
. . . . . . . . . . . . . . 15
|
58 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
++ ++ |
59 | 58 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
++ ++ |
60 | 59 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
++ ++ |
61 | 57, 60 | syl5bb 272 |
. . . . . . . . . . . . . 14
++
++ |
62 | 61, 3 | elrab2 3366 |
. . . . . . . . . . . . 13
++
++ ClWalks
++ |
63 | 34, 55, 62 | sylanbrc 698 |
. . . . . . . . . . . 12
++ ClWalks
FinUSGraph
Word
Vtx
++ |
64 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks |
65 | 64 | opeq2d 4409 |
. . . . . . . . . . . . . . . . 17
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks |
66 | 65 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ substr
++ substr
|
67 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ ClWalks |
68 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks
|
69 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
70 | 69 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
71 | 70 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . . . . 22
++ ClWalks
++ ClWalks |
72 | 71 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . 21
FinUSGraph Word
Vtx
++ ClWalks
++ ClWalks |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks
++ ClWalks
|
74 | 68, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks
|
75 | 74 | imp 445 |
. . . . . . . . . . . . . . . . . 18
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks |
76 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
++ ++ |
77 | 76 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
++ ++ |
78 | 59, 77 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
++ |
79 | 78 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
++ |
80 | 57, 79 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . 19
++
|
81 | 80, 3 | elrab2 3366 |
. . . . . . . . . . . . . . . . . 18
++
++ ClWalks
|
82 | 67, 75, 81 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ |
83 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
++ substr
|
84 | 56 | opeq2i 4406 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 2, 84 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . 19
substr substr |
86 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
++ ++ |
87 | 59 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . . . . 21
++
++ |
88 | 86, 87 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
++ substr ++ substr ++ |
89 | 45, 46 | op2nd 7177 |
. . . . . . . . . . . . . . . . . . . . 21
++ ++ |
90 | 47 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . 22
++ |
91 | 90 | opeq2i 4406 |
. . . . . . . . . . . . . . . . . . . . 21
++ |
92 | 89, 91 | oveq12i 6662 |
. . . . . . . . . . . . . . . . . . . 20
++ substr ++ ++ substr
|
93 | 88, 92 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
++ substr ++ substr
|
94 | 85, 93 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
++ substr ++ substr
|
95 | 94, 4 | fvmptg 6280 |
. . . . . . . . . . . . . . . . 17
++ ++ substr ++ ++ substr |
96 | 82, 83, 95 | sylancl 694 |
. . . . . . . . . . . . . . . 16
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ ++ substr |
97 | 40 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks Word
Vtx
|
98 | | simpl 473 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx Word Vtx |
99 | | wrdsymb1 13342 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx Vtx |
100 | 99 | s1cld 13383 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx Word
Vtx |
101 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx |
102 | | swrdccatid 13497 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx Word Vtx ++ substr
|
103 | 98, 100, 101, 102 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ++ substr
|
104 | 103 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Word Vtx ++ substr |
105 | 97, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ substr |
106 | 66, 96, 105 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . . 15
++ ClWalks FinUSGraph Word
Vtx
++ ClWalks ++ |
107 | 106 | ex 450 |
. . . . . . . . . . . . . 14
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks
++ |
108 | 107 | adantr 481 |
. . . . . . . . . . . . 13
++ ClWalks FinUSGraph Word
Vtx
++ ++ ClWalks ++ |
109 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
++ ++ |
110 | 109 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
++
++ |
111 | 110 | imbi2d 330 |
. . . . . . . . . . . . . 14
++ ++ ClWalks
++ ClWalks
++ |
112 | 111 | adantl 482 |
. . . . . . . . . . . . 13
++ ClWalks FinUSGraph Word
Vtx
++ ++ ClWalks
++ ClWalks
++ |
113 | 108, 112 | mpbird 247 |
. . . . . . . . . . . 12
++ ClWalks FinUSGraph Word
Vtx
++ ++ ClWalks |
114 | 63, 113 | rspcimedv 3311 |
. . . . . . . . . . 11
++ ClWalks
FinUSGraph
Word
Vtx
++ ClWalks
|
115 | 114 | ex 450 |
. . . . . . . . . 10
++ ClWalks
FinUSGraph Word
Vtx
++ ClWalks
|
116 | 115 | pm2.43b 55 |
. . . . . . . . 9
FinUSGraph Word
Vtx
++ ClWalks
|
117 | 33, 116 | syl5bi 232 |
. . . . . . . 8
FinUSGraph Word
Vtx
ClWalks ++
|
118 | 117 | exlimdv 1861 |
. . . . . . 7
FinUSGraph Word
Vtx
ClWalks ++
|
119 | 118 | adantrd 484 |
. . . . . 6
FinUSGraph Word
Vtx
ClWalks ++
|
120 | 32, 119 | sylbid 230 |
. . . . 5
FinUSGraph Word
Vtx
ClWWalksN
|
121 | 120 | impancom 456 |
. . . 4
FinUSGraph ClWWalksN
Word
Vtx
|
122 | 8, 121 | mpd 15 |
. . 3
FinUSGraph ClWWalksN
|
123 | 122 | ralrimiva 2966 |
. 2
FinUSGraph
ClWWalksN
|
124 | | dffo3 6374 |
. 2
ClWWalksN
ClWWalksN ClWWalksN
|
125 | 5, 123, 124 | sylanbrc 698 |
1
FinUSGraph
ClWWalksN |