Step | Hyp | Ref
| Expression |
1 | | wlkp1.v |
. . . 4
Vtx |
2 | | wlkp1.i |
. . . 4
iEdg |
3 | | wlkp1.f |
. . . 4
|
4 | | wlkp1.a |
. . . 4
|
5 | | wlkp1.b |
. . . 4
|
6 | | wlkp1.c |
. . . 4
|
7 | | wlkp1.d |
. . . 4
|
8 | | wlkp1.w |
. . . 4
Walks |
9 | | wlkp1.n |
. . . 4
|
10 | | wlkp1.e |
. . . 4
Edg |
11 | | wlkp1.x |
. . . 4
|
12 | | wlkp1.u |
. . . 4
iEdg |
13 | | wlkp1.h |
. . . 4
|
14 | | wlkp1.q |
. . . 4
|
15 | | wlkp1.s |
. . . 4
Vtx |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem6 26575 |
. . 3
..^ iEdg |
17 | 10 | elfvexd 6222 |
. . . . . 6
|
18 | 1, 2 | iswlkg 26509 |
. . . . . 6
Walks Word ..^if- |
19 | 17, 18 | syl 17 |
. . . . 5
Walks
Word ..^if- |
20 | 9 | eqcomi 2631 |
. . . . . . . . 9
|
21 | 20 | oveq2i 6661 |
. . . . . . . 8
..^ ..^ |
22 | 21 | raleqi 3142 |
. . . . . . 7
..^if-
..^if- |
23 | 22 | biimpi 206 |
. . . . . 6
..^if- ..^if- |
24 | 23 | 3ad2ant3 1084 |
. . . . 5
Word ..^if-
..^if- |
25 | 19, 24 | syl6bi 243 |
. . . 4
Walks
..^if- |
26 | 8, 25 | mpd 15 |
. . 3
..^if- |
27 | | eqeq12 2635 |
. . . . . . 7
|
28 | 27 | 3adant3 1081 |
. . . . . 6
iEdg
|
29 | | simp3 1063 |
. . . . . . 7
iEdg
iEdg |
30 | | simp1 1061 |
. . . . . . . 8
iEdg
|
31 | 30 | sneqd 4189 |
. . . . . . 7
iEdg
|
32 | 29, 31 | eqeq12d 2637 |
. . . . . 6
iEdg
iEdg
|
33 | | preq12 4270 |
. . . . . . . 8
|
34 | 33 | 3adant3 1081 |
. . . . . . 7
iEdg
|
35 | 34, 29 | sseq12d 3634 |
. . . . . 6
iEdg
iEdg
|
36 | 28, 32, 35 | ifpbi123d 1027 |
. . . . 5
iEdg
if- iEdg
iEdg
if- |
37 | 36 | biimprd 238 |
. . . 4
iEdg
if- if- iEdg iEdg |
38 | 37 | ral2imi 2947 |
. . 3
..^ iEdg
..^if- ..^if- iEdg
iEdg |
39 | 16, 26, 38 | sylc 65 |
. 2
..^if- iEdg
iEdg |
40 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | wlkp1lem3 26572 |
. . . . 5
iEdg |
41 | 40 | adantr 481 |
. . . 4
iEdg |
42 | 5, 10, 7 | 3jca 1242 |
. . . . . 6
Edg
|
43 | 42 | adantr 481 |
. . . . 5
Edg |
44 | | fsnunfv 6453 |
. . . . 5
Edg
|
45 | 43, 44 | syl 17 |
. . . 4
|
46 | | fveq2 6191 |
. . . . . . . 8
|
47 | | fveq2 6191 |
. . . . . . . 8
|
48 | 46, 47 | eqeq12d 2637 |
. . . . . . 7
|
49 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem5 26574 |
. . . . . . 7
|
50 | 2 | wlkf 26510 |
. . . . . . . . . 10
Walks Word |
51 | | lencl 13324 |
. . . . . . . . . . 11
Word
|
52 | 9 | eleq1i 2692 |
. . . . . . . . . . . 12
|
53 | | elnn0uz 11725 |
. . . . . . . . . . . 12
|
54 | 52, 53 | sylbb1 227 |
. . . . . . . . . . 11
|
55 | 51, 54 | syl 17 |
. . . . . . . . . 10
Word
|
56 | 8, 50, 55 | 3syl 18 |
. . . . . . . . 9
|
57 | 56, 53 | sylibr 224 |
. . . . . . . 8
|
58 | | nn0fz0 12437 |
. . . . . . . 8
|
59 | 57, 58 | sylib 208 |
. . . . . . 7
|
60 | 48, 49, 59 | rspcdva 3316 |
. . . . . 6
|
61 | 14 | fveq1i 6192 |
. . . . . . . . . . 11
|
62 | | ovex 6678 |
. . . . . . . . . . . 12
|
63 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | wlkp1lem1 26570 |
. . . . . . . . . . . 12
|
64 | | fsnunfv 6453 |
. . . . . . . . . . . 12
|
65 | 62, 6, 63, 64 | mp3an2i 1429 |
. . . . . . . . . . 11
|
66 | 61, 65 | syl5eq 2668 |
. . . . . . . . . 10
|
67 | 66 | eqeq2d 2632 |
. . . . . . . . 9
|
68 | | eqcom 2629 |
. . . . . . . . 9
|
69 | 67, 68 | syl6bb 276 |
. . . . . . . 8
|
70 | | wlkp1.l |
. . . . . . . . . 10
|
71 | | sneq 4187 |
. . . . . . . . . . 11
|
72 | 71 | adantl 482 |
. . . . . . . . . 10
|
73 | 70, 72 | eqtrd 2656 |
. . . . . . . . 9
|
74 | 73 | ex 450 |
. . . . . . . 8
|
75 | 69, 74 | sylbid 230 |
. . . . . . 7
|
76 | | eqeq1 2626 |
. . . . . . . 8
|
77 | | sneq 4187 |
. . . . . . . . 9
|
78 | 77 | eqeq2d 2632 |
. . . . . . . 8
|
79 | 76, 78 | imbi12d 334 |
. . . . . . 7
|
80 | 75, 79 | syl5ibrcom 237 |
. . . . . 6
|
81 | 60, 80 | mpd 15 |
. . . . 5
|
82 | 81 | imp 445 |
. . . 4
|
83 | 41, 45, 82 | 3eqtrd 2660 |
. . 3
iEdg |
84 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | wlkp1lem7 26576 |
. . . 4
iEdg |
85 | 84 | adantr 481 |
. . 3
iEdg |
86 | 83, 85 | ifpimpda 1028 |
. 2
if- iEdg
iEdg |
87 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | wlkp1lem2 26571 |
. . . . . 6
|
88 | 87 | oveq2d 6666 |
. . . . 5
..^ ..^ |
89 | | fzosplitsn 12576 |
. . . . . 6
..^ ..^ |
90 | 56, 89 | syl 17 |
. . . . 5
..^ ..^ |
91 | 88, 90 | eqtrd 2656 |
. . . 4
..^ ..^ |
92 | 91 | raleqdv 3144 |
. . 3
..^if- iEdg
iEdg
..^ if- iEdg iEdg |
93 | | ralunb 3794 |
. . . 4
..^ if- iEdg iEdg
..^if- iEdg iEdg
if- iEdg iEdg |
94 | 93 | a1i 11 |
. . 3
..^ if- iEdg iEdg
..^if- iEdg iEdg
if- iEdg iEdg |
95 | | fvex 6201 |
. . . . . 6
|
96 | 9, 95 | eqeltri 2697 |
. . . . 5
|
97 | | fveq2 6191 |
. . . . . . . 8
|
98 | | oveq1 6657 |
. . . . . . . . 9
|
99 | 98 | fveq2d 6195 |
. . . . . . . 8
|
100 | 97, 99 | eqeq12d 2637 |
. . . . . . 7
|
101 | | fveq2 6191 |
. . . . . . . . 9
|
102 | 101 | fveq2d 6195 |
. . . . . . . 8
iEdg iEdg |
103 | 97 | sneqd 4189 |
. . . . . . . 8
|
104 | 102, 103 | eqeq12d 2637 |
. . . . . . 7
iEdg
iEdg |
105 | 97, 99 | preq12d 4276 |
. . . . . . . 8
|
106 | 105, 102 | sseq12d 3634 |
. . . . . . 7
iEdg
iEdg |
107 | 100, 104,
106 | ifpbi123d 1027 |
. . . . . 6
if- iEdg iEdg
if-
iEdg iEdg |
108 | 107 | ralsng 4218 |
. . . . 5
if- iEdg iEdg
if-
iEdg iEdg |
109 | 96, 108 | mp1i 13 |
. . . 4
if- iEdg
iEdg
if-
iEdg iEdg |
110 | 109 | anbi2d 740 |
. . 3
..^if- iEdg iEdg if- iEdg iEdg ..^if- iEdg iEdg if- iEdg
iEdg |
111 | 92, 94, 110 | 3bitrd 294 |
. 2
..^if- iEdg
iEdg
..^if- iEdg iEdg if- iEdg
iEdg |
112 | 39, 86, 111 | mpbir2and 957 |
1
..^if- iEdg iEdg |