Proof of Theorem elwwlks2
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. . 3
|
2 | | elwwlks2.v |
. . . 4
Vtx |
3 | 2 | wwlksnwwlksnon 26810 |
. . 3
UPGraph
WWalksN
WWalksNOn |
4 | 1, 3 | mpan 706 |
. 2
UPGraph WWalksN
WWalksNOn
|
5 | 2 | elwwlks2on 26852 |
. . . 4
UPGraph
WWalksNOn
Walks |
6 | 5 | 3expb 1266 |
. . 3
UPGraph
WWalksNOn
Walks |
7 | 6 | 2rexbidva 3056 |
. 2
UPGraph
WWalksNOn
Walks |
8 | | rexcom 3099 |
. . . 4
Walks
Walks |
9 | | s3cli 13626 |
. . . . . . . . . 10
Word |
10 | 9 | a1i 11 |
. . . . . . . . 9
UPGraph
Word |
11 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
UPGraph
|
12 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
UPGraph
|
13 | 11, 12 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
UPGraph
|
14 | 13 | breq2d 4665 |
. . . . . . . . . . . . . . 15
UPGraph
Walks
Walks |
15 | 14 | biimpd 219 |
. . . . . . . . . . . . . 14
UPGraph
Walks Walks |
16 | 15 | com12 32 |
. . . . . . . . . . . . 13
Walks UPGraph
Walks |
17 | 16 | adantr 481 |
. . . . . . . . . . . 12
Walks UPGraph
Walks |
18 | 17 | impcom 446 |
. . . . . . . . . . 11
UPGraph
Walks Walks |
19 | | simprr 796 |
. . . . . . . . . . 11
UPGraph
Walks |
20 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
21 | | s3fv0 13636 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
23 | 20, 22 | mp1i 13 |
. . . . . . . . . . . . . . 15
|
24 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
25 | 23, 24 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
26 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
27 | | s3fv1 13637 |
. . . . . . . . . . . . . . . . 17
|
28 | 27 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
29 | 26, 28 | mp1i 13 |
. . . . . . . . . . . . . . 15
|
30 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
31 | 29, 30 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
32 | | vex 3203 |
. . . . . . . . . . . . . . . 16
|
33 | | s3fv2 13638 |
. . . . . . . . . . . . . . . . 17
|
34 | 33 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
|
35 | 32, 34 | mp1i 13 |
. . . . . . . . . . . . . . 15
|
36 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
37 | 35, 36 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
38 | 25, 31, 37 | 3jca 1242 |
. . . . . . . . . . . . 13
|
39 | 38 | adantl 482 |
. . . . . . . . . . . 12
UPGraph
|
40 | 39 | adantr 481 |
. . . . . . . . . . 11
UPGraph
Walks
|
41 | 18, 19, 40 | 3jca 1242 |
. . . . . . . . . 10
UPGraph
Walks Walks
|
42 | 41 | ex 450 |
. . . . . . . . 9
UPGraph
Walks Walks
|
43 | 10, 42 | spcimedv 3292 |
. . . . . . . 8
UPGraph
Walks Walks
|
44 | | wlklenvp1 26514 |
. . . . . . . . . . . . . . . . . . . . . . 23
Walks
|
45 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
46 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
48 | 45, 47 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Walks |
50 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
51 | 49, 50 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Walks |
52 | 51 | exp32 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
Walks
|
53 | 44, 52 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
Walks
|
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
Walks UPGraph
|
55 | 54 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
Walks UPGraph
|
56 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
|
57 | 56 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
|
59 | 58 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
|
61 | 60 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | 57, 59, 61 | 3anim123i 1247 |
. . . . . . . . . . . . . . . . . . . 20
|
63 | 55, 62 | anim12i 590 |
. . . . . . . . . . . . . . . . . . 19
Walks UPGraph
|
64 | 2 | wlkpwrd 26513 |
. . . . . . . . . . . . . . . . . . . . . 22
Walks
Word |
65 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
UPGraph
|
66 | 65 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
UPGraph
|
67 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
68 | 66, 67 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
UPGraph
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
UPGraph
|
70 | 64, 69 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . 21
Walks UPGraph
Word
|
71 | 70 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
Walks UPGraph
Word
|
72 | | eqwrds3 13704 |
. . . . . . . . . . . . . . . . . . . 20
Word
|
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
Walks UPGraph
|
74 | 63, 73 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
Walks UPGraph
|
75 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
Walks UPGraph
|
76 | 75 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
Walks UPGraph
|
77 | 74, 76 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
Walks UPGraph
|
78 | 77 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
Walks UPGraph
Walks Walks |
79 | 78 | biimpd 219 |
. . . . . . . . . . . . . . 15
Walks UPGraph
Walks
Walks |
80 | | simplr 792 |
. . . . . . . . . . . . . . 15
Walks UPGraph
|
81 | 79, 80 | jctird 567 |
. . . . . . . . . . . . . 14
Walks UPGraph
Walks
Walks |
82 | 81 | exp41 638 |
. . . . . . . . . . . . 13
Walks
UPGraph
Walks Walks |
83 | 82 | com25 99 |
. . . . . . . . . . . 12
Walks
Walks
UPGraph
Walks |
84 | 83 | pm2.43i 52 |
. . . . . . . . . . 11
Walks
UPGraph
Walks |
85 | 84 | 3imp 1256 |
. . . . . . . . . 10
Walks UPGraph
Walks |
86 | 85 | com12 32 |
. . . . . . . . 9
UPGraph
Walks
Walks |
87 | 86 | exlimdv 1861 |
. . . . . . . 8
UPGraph
Walks
Walks |
88 | 43, 87 | impbid 202 |
. . . . . . 7
UPGraph
Walks Walks
|
89 | 88 | exbidv 1850 |
. . . . . 6
UPGraph
Walks
Walks
|
90 | 89 | pm5.32da 673 |
. . . . 5
UPGraph
Walks Walks
|
91 | 90 | 2rexbidva 3056 |
. . . 4
UPGraph
Walks
Walks
|
92 | 8, 91 | syl5bb 272 |
. . 3
UPGraph
Walks
Walks
|
93 | 92 | rexbidva 3049 |
. 2
UPGraph
Walks
Walks
|
94 | 4, 7, 93 | 3bitrd 294 |
1
UPGraph WWalksN
Walks
|