Step | Hyp | Ref
| Expression |
1 | | wlkv 26508 |
. 2
Walks
|
2 | | eqid 2622 |
. . . 4
Vtx Vtx |
3 | | eqid 2622 |
. . . 4
iEdg iEdg |
4 | 2, 3 | iswlk 26506 |
. . 3
Walks Word iEdg Vtx
..^if- iEdg iEdg |
5 | | fvex 6201 |
. . . . . . 7
|
6 | 5 | inex1 4799 |
. . . . . 6
|
7 | | fzo0ss1 12498 |
. . . . . . . . . . . 12
..^ ..^ |
8 | 7 | sseli 3599 |
. . . . . . . . . . 11
..^
..^ |
9 | | wkslem1 26503 |
. . . . . . . . . . . 12
if- iEdg iEdg
if- iEdg iEdg |
10 | 9 | rspcv 3305 |
. . . . . . . . . . 11
..^
..^if- iEdg iEdg if- iEdg iEdg |
11 | 8, 10 | syl 17 |
. . . . . . . . . 10
..^
..^if- iEdg iEdg if- iEdg iEdg |
12 | 11 | imp 445 |
. . . . . . . . 9
..^
..^if- iEdg iEdg if- iEdg iEdg |
13 | | elfzofz 12485 |
. . . . . . . . . . 11
..^
|
14 | | fz1fzo0m1 12515 |
. . . . . . . . . . 11
..^ |
15 | | wkslem1 26503 |
. . . . . . . . . . . 12
if- iEdg iEdg
if- iEdg iEdg |
16 | 15 | rspcv 3305 |
. . . . . . . . . . 11
..^
..^if- iEdg iEdg if- iEdg iEdg |
17 | 13, 14, 16 | 3syl 18 |
. . . . . . . . . 10
..^
..^if- iEdg iEdg if- iEdg iEdg |
18 | 17 | imp 445 |
. . . . . . . . 9
..^
..^if- iEdg iEdg if- iEdg iEdg |
19 | | df-ifp 1013 |
. . . . . . . . . . . 12
if- iEdg
iEdg
iEdg iEdg |
20 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
..^
|
21 | | zcn 11382 |
. . . . . . . . . . . . . . 15
|
22 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
23 | | npcan1 10455 |
. . . . . . . . . . . . . . . 16
|
24 | | wkslem2 26504 |
. . . . . . . . . . . . . . . 16
if- iEdg iEdg
if- iEdg iEdg |
25 | 22, 23, 24 | syl2anc 693 |
. . . . . . . . . . . . . . 15
if- iEdg iEdg
if- iEdg iEdg |
26 | 20, 21, 25 | 3syl 18 |
. . . . . . . . . . . . . 14
..^
if- iEdg
iEdg
if- iEdg iEdg |
27 | | df-ifp 1013 |
. . . . . . . . . . . . . . 15
if- iEdg
iEdg
iEdg
iEdg |
28 | | sneq 4187 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
29 | 28 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg
iEdg |
30 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
31 | 30 | snid 4208 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
32 | | wlk1walk.i |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
iEdg |
33 | 32 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
iEdg |
34 | 33 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg |
35 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg iEdg |
36 | 34, 35 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg
|
37 | 31, 36 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg |
38 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg iEdg |
39 | 31, 38 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg iEdg |
40 | 32 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg |
41 | 39, 40 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg |
42 | 37, 41 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg iEdg |
43 | 42 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg |
44 | 29, 43 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg iEdg |
45 | 44 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
iEdg iEdg
|
46 | 45 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
iEdg iEdg |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
iEdg
iEdg |
48 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
49 | 30, 48 | prss 4351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg
iEdg
iEdg |
50 | 32 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
iEdg |
51 | 50 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
iEdg |
52 | 51 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
iEdg |
53 | 52 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg
iEdg |
55 | 49, 54 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg
|
56 | 37, 55 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg iEdg |
57 | 56 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg
iEdg
|
58 | 29, 57 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg
iEdg
|
59 | 58 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
iEdg iEdg |
60 | 59 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
iEdg
iEdg |
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
iEdg
iEdg |
62 | 47, 61 | jaoi 394 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg
iEdg |
63 | 62 | com12 32 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg |
64 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 64, 30 | prss 4351 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg
iEdg |
66 | 50 | fveq1i 6192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
iEdg |
67 | 66 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg |
68 | 67 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg
|
69 | 40 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
iEdg |
70 | 69, 38 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg
|
71 | 31, 70 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg |
72 | 68, 71 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg iEdg |
73 | 72 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg
iEdg |
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg iEdg
|
75 | 65, 74 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg
iEdg |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
iEdg iEdg
|
77 | 76 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
iEdg
iEdg |
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
iEdg iEdg |
79 | 67, 52 | anbi12i 733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
iEdg iEdg |
80 | 79 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
iEdg iEdg |
81 | 80 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
iEdg
iEdg |
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg iEdg iEdg |
83 | 65, 82 | sylbir 225 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg
iEdg |
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg iEdg |
85 | 84 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg
iEdg |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
iEdg
iEdg iEdg |
87 | 49, 86 | sylbir 225 |
. . . . . . . . . . . . . . . . . . 19
iEdg
iEdg |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
iEdg iEdg |
89 | 78, 88 | jaoi 394 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg iEdg |
90 | 89 | com12 32 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg |
91 | 63, 90 | jaoi 394 |
. . . . . . . . . . . . . . 15
iEdg iEdg iEdg iEdg |
92 | 27, 91 | sylbi 207 |
. . . . . . . . . . . . . 14
if- iEdg
iEdg iEdg iEdg |
93 | 26, 92 | syl6bi 243 |
. . . . . . . . . . . . 13
..^
if- iEdg
iEdg iEdg iEdg |
94 | 93 | com3r 87 |
. . . . . . . . . . . 12
iEdg iEdg ..^ if- iEdg iEdg |
95 | 19, 94 | sylbi 207 |
. . . . . . . . . . 11
if- iEdg
iEdg ..^ if- iEdg iEdg |
96 | 95 | com12 32 |
. . . . . . . . . 10
..^
if- iEdg
iEdg if- iEdg iEdg |
97 | 96 | adantr 481 |
. . . . . . . . 9
..^
..^if- iEdg iEdg if- iEdg iEdg if- iEdg iEdg |
98 | 12, 18, 97 | mp2d 49 |
. . . . . . . 8
..^
..^if- iEdg iEdg |
99 | 98 | ancoms 469 |
. . . . . . 7
..^if- iEdg iEdg ..^ |
100 | | inelcm 4032 |
. . . . . . 7
|
101 | 99, 100 | syl 17 |
. . . . . 6
..^if- iEdg iEdg ..^ |
102 | | hashge1 13178 |
. . . . . 6
|
103 | 6, 101, 102 | sylancr 695 |
. . . . 5
..^if- iEdg iEdg ..^ |
104 | 103 | ralrimiva 2966 |
. . . 4
..^if- iEdg iEdg ..^ |
105 | 104 | 3ad2ant3 1084 |
. . 3
Word iEdg Vtx
..^if- iEdg iEdg
..^ |
106 | 4, 105 | syl6bi 243 |
. 2
Walks ..^ |
107 | 1, 106 | mpcom 38 |
1
Walks ..^ |