Description: F is a function from the nonempty closed walks into the closed walks as word in a simple pseudograph. (Contributed by AV, 23-May-2022) (Revised by AV, 29-Oct-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clwlkclwwlkf.c | |
|
clwlkclwwlkf.f | |
||
Assertion | clwlkclwwlkf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clwlkclwwlkf.c | |
|
2 | clwlkclwwlkf.f | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 1 3 4 | clwlkclwwlkflem | |
6 | isclwlk | |
|
7 | fvex | |
|
8 | breq1 | |
|
9 | 7 8 | spcev | |
10 | 6 9 | sylbir | |
11 | 10 | 3adant3 | |
12 | 11 | adantl | |
13 | simpl | |
|
14 | eqid | |
|
15 | 14 | wlkpwrd | |
16 | 15 | 3ad2ant1 | |
17 | 16 | adantl | |
18 | elnnnn0c | |
|
19 | nn0re | |
|
20 | 1e2m1 | |
|
21 | 20 | breq1i | |
22 | 21 | biimpi | |
23 | 2re | |
|
24 | 1re | |
|
25 | lesubadd | |
|
26 | 23 24 25 | mp3an12 | |
27 | 22 26 | syl5ib | |
28 | 19 27 | syl | |
29 | 28 | adantl | |
30 | wlklenvp1 | |
|
31 | 30 | adantr | |
32 | 31 | breq2d | |
33 | 29 32 | sylibrd | |
34 | 33 | expimpd | |
35 | 18 34 | syl5bi | |
36 | 35 | a1d | |
37 | 36 | 3imp | |
38 | 37 | adantl | |
39 | eqid | |
|
40 | 14 39 | clwlkclwwlk | |
41 | 13 17 38 40 | syl3anc | |
42 | 12 41 | mpbid | |
43 | 5 42 | sylan2 | |
44 | 43 | simprd | |
45 | 44 2 | fmptd | |