Proof of Theorem elwspths2spth
Step | Hyp | Ref
| Expression |
1 | | 2nn0 11309 |
. . 3
|
2 | | elwwlks2.v |
. . . 4
Vtx |
3 | 2 | wspthsnwspthsnon 26811 |
. . 3
UPGraph
WSPathsN
WSPathsNOn |
4 | 1, 3 | mpan 706 |
. 2
UPGraph WSPathsN
WSPathsNOn
|
5 | 2 | elwspths2on 26853 |
. . . 4
UPGraph
WSPathsNOn
WSPathsNOn
|
6 | 5 | 3expb 1266 |
. . 3
UPGraph
WSPathsNOn
WSPathsNOn |
7 | 6 | 2rexbidva 3056 |
. 2
UPGraph
WSPathsNOn
WSPathsNOn |
8 | | rexcom 3099 |
. . . 4
WSPathsNOn
WSPathsNOn |
9 | | simpr 477 |
. . . . . . . . . 10
UPGraph
|
10 | | simpr 477 |
. . . . . . . . . 10
|
11 | 9, 10 | anim12i 590 |
. . . . . . . . 9
UPGraph
|
12 | 2 | wspthnon 26743 |
. . . . . . . . 9
WSPathsNOn WWalksNOn SPathsOn |
13 | 11, 12 | syl 17 |
. . . . . . . 8
UPGraph
WSPathsNOn
WWalksNOn SPathsOn |
14 | 13 | adantr 481 |
. . . . . . 7
UPGraph
WSPathsNOn WWalksNOn SPathsOn |
15 | | ancom 466 |
. . . . . . . . 9
WWalksNOn SPathsOn SPathsOn WWalksNOn |
16 | | 19.41v 1914 |
. . . . . . . . 9
SPathsOn WWalksNOn
SPathsOn WWalksNOn |
17 | 15, 16 | bitr4i 267 |
. . . . . . . 8
WWalksNOn SPathsOn SPathsOn WWalksNOn |
18 | | vex 3203 |
. . . . . . . . . . . . . 14
|
19 | | s3cli 13626 |
. . . . . . . . . . . . . 14
Word |
20 | 18, 19 | pm3.2i 471 |
. . . . . . . . . . . . 13
Word
|
21 | 2 | isspthonpth 26645 |
. . . . . . . . . . . . 13
Word SPathsOn SPaths |
22 | 11, 20, 21 | sylancl 694 |
. . . . . . . . . . . 12
UPGraph
SPathsOn
SPaths |
23 | 2 | wwlknon 26742 |
. . . . . . . . . . . . . 14
WWalksNOn
WWalksN |
24 | 11, 23 | syl 17 |
. . . . . . . . . . . . 13
UPGraph
WWalksNOn
WWalksN |
25 | | iswwlksn 26730 |
. . . . . . . . . . . . . . . 16
WWalksN
WWalks |
26 | 1, 25 | ax-mp 5 |
. . . . . . . . . . . . . . 15
WWalksN
WWalks |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
UPGraph
WWalksN
WWalks |
28 | 27 | 3anbi1d 1403 |
. . . . . . . . . . . . 13
UPGraph
WWalksN WWalks |
29 | 24, 28 | bitrd 268 |
. . . . . . . . . . . 12
UPGraph
WWalksNOn
WWalks |
30 | 22, 29 | anbi12d 747 |
. . . . . . . . . . 11
UPGraph
SPathsOn WWalksNOn
SPaths WWalks |
31 | 30 | adantr 481 |
. . . . . . . . . 10
UPGraph
SPathsOn WWalksNOn
SPaths WWalks |
32 | 19 | a1i 11 |
. . . . . . . . . . . . 13
UPGraph
Word |
33 | | simprl1 1106 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths WWalks SPaths |
34 | | spthiswlk 26624 |
. . . . . . . . . . . . . . . . . . . 20
SPaths Walks |
35 | | wlklenvm1 26517 |
. . . . . . . . . . . . . . . . . . . 20
Walks |
36 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
WWalks
|
37 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
39 | | pncan1 10454 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
41 | 37, 40 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
WWalks |
43 | 42 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . 23
WWalks |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
WWalks
|
45 | 36, 44 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
WWalks
|
46 | 45 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
WWalks |
47 | 34, 35, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
SPaths WWalks |
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . 18
SPaths WWalks |
49 | 48 | imp 445 |
. . . . . . . . . . . . . . . . 17
SPaths WWalks
|
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths WWalks |
51 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
52 | | s3fv0 13636 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 53 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
|
55 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
56 | | s3fv1 13637 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 57 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
|
59 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . 20
|
60 | | s3fv2 13638 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
62 | 61 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . 18
|
63 | 54, 58, 62 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths WWalks
|
65 | 33, 50, 64 | 3jca 1242 |
. . . . . . . . . . . . . . 15
UPGraph
SPaths WWalks SPaths |
66 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
SPaths
SPaths |
67 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 67 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
69 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
|
70 | 69 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
71 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . 19
|
72 | 71 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
73 | 68, 70, 72 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . 17
|
74 | 66, 73 | 3anbi13d 1401 |
. . . . . . . . . . . . . . . 16
SPaths
SPaths
|
75 | 74 | ad2antlr 763 |
. . . . . . . . . . . . . . 15
UPGraph
SPaths WWalks SPaths
SPaths
|
76 | 65, 75 | mpbird 247 |
. . . . . . . . . . . . . 14
UPGraph
SPaths WWalks SPaths |
77 | 76 | ex 450 |
. . . . . . . . . . . . 13
UPGraph
SPaths WWalks
SPaths
|
78 | 32, 77 | spcimedv 3292 |
. . . . . . . . . . . 12
UPGraph
SPaths WWalks
SPaths
|
79 | | spthiswlk 26624 |
. . . . . . . . . . . . . . . . . . . . 21
SPaths
Walks |
80 | | wlklenvp1 26514 |
. . . . . . . . . . . . . . . . . . . . 21
Walks
|
81 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
83 | 81, 82 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | 83 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
|
85 | 84 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . 21
|
86 | 79, 80, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
SPaths
|
87 | 86 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
SPaths |
88 | 87 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
SPaths |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
|
90 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . 21
|
93 | 90, 91, 92 | 3anbi123i 1251 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | 93 | biimpi 206 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 94 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . 18
SPaths |
96 | 95 | adantl 482 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
|
97 | 89, 96 | jca 554 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths
|
98 | 2 | wlkpwrd 26513 |
. . . . . . . . . . . . . . . . . . 19
Walks
Word |
99 | 79, 98 | syl 17 |
. . . . . . . . . . . . . . . . . 18
SPaths
Word |
100 | 99 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . 17
SPaths Word |
101 | 9 | anim1i 592 |
. . . . . . . . . . . . . . . . . 18
UPGraph
|
102 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . 18
|
103 | 101, 102 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
UPGraph
|
104 | | eqwrds3 13704 |
. . . . . . . . . . . . . . . . 17
Word
|
105 | 100, 103,
104 | syl2anr 495 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths
|
106 | 97, 105 | mpbird 247 |
. . . . . . . . . . . . . . 15
UPGraph
SPaths
|
107 | 66 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . 20
SPaths
SPaths |
108 | 107 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . 19
SPaths SPaths |
109 | 108 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
UPGraph
SPaths
SPaths |
110 | 109 | imp 445 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
SPaths |
111 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
|
112 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
113 | 112, 61 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
|
114 | 113 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . 18
SPaths |
115 | 114 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
|
116 | 110, 111,
115 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths
SPaths |
117 | | wlkiswwlks1 26753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
UPGraph Walks
WWalks |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
UPGraph
Walks WWalks |
119 | 118 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
UPGraph
Walks
WWalks |
120 | 79, 119 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . 22
SPaths
UPGraph
WWalks |
121 | 120 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . 21
SPaths UPGraph
WWalks |
122 | 121 | impcom 446 |
. . . . . . . . . . . . . . . . . . . 20
UPGraph
SPaths
WWalks |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
UPGraph
SPaths
WWalks |
124 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
WWalks
WWalks |
125 | 124 | bicomd 213 |
. . . . . . . . . . . . . . . . . . . 20
WWalks
WWalks |
126 | 125 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
UPGraph
SPaths
WWalks WWalks |
127 | 123, 126 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
UPGraph
SPaths
WWalks |
128 | | s3len 13639 |
. . . . . . . . . . . . . . . . . . 19
|
129 | | df-3 11080 |
. . . . . . . . . . . . . . . . . . 19
|
130 | 128, 129 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
131 | 127, 130 | jctir 561 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
WWalks |
132 | 61 | a1i 11 |
. . . . . . . . . . . . . . . . 17
UPGraph
SPaths
|
133 | 131, 111,
132 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
UPGraph
SPaths
WWalks |
134 | 116, 133 | jca 554 |
. . . . . . . . . . . . . . 15
UPGraph
SPaths
SPaths WWalks |
135 | 106, 134 | mpdan 702 |
. . . . . . . . . . . . . 14
UPGraph
SPaths
SPaths WWalks |
136 | 135 | ex 450 |
. . . . . . . . . . . . 13
UPGraph
SPaths SPaths WWalks |
137 | 136 | exlimdv 1861 |
. . . . . . . . . . . 12
UPGraph
SPaths
SPaths WWalks |
138 | 78, 137 | impbid 202 |
. . . . . . . . . . 11
UPGraph
SPaths WWalks SPaths
|
139 | 138 | adantr 481 |
. . . . . . . . . 10
UPGraph
SPaths WWalks SPaths
|
140 | 31, 139 | bitrd 268 |
. . . . . . . . 9
UPGraph
SPathsOn WWalksNOn
SPaths
|
141 | 140 | exbidv 1850 |
. . . . . . . 8
UPGraph
SPathsOn WWalksNOn SPaths |
142 | 17, 141 | syl5bb 272 |
. . . . . . 7
UPGraph
WWalksNOn SPathsOn SPaths
|
143 | 14, 142 | bitrd 268 |
. . . . . 6
UPGraph
WSPathsNOn SPaths |
144 | 143 | pm5.32da 673 |
. . . . 5
UPGraph
WSPathsNOn
SPaths
|
145 | 144 | 2rexbidva 3056 |
. . . 4
UPGraph
WSPathsNOn
SPaths
|
146 | 8, 145 | syl5bb 272 |
. . 3
UPGraph
WSPathsNOn
SPaths
|
147 | 146 | rexbidva 3049 |
. 2
UPGraph
WSPathsNOn
SPaths
|
148 | 4, 7, 147 | 3bitrd 294 |
1
UPGraph WSPathsN
SPaths
|