Step | Hyp | Ref
| Expression |
1 | | umgrupgr 25998 |
. . . 4
UMGraph UPGraph |
2 | 1 | adantr 481 |
. . 3
UMGraph
UPGraph |
3 | | simp1 1061 |
. . . 4
|
4 | 3 | adantl 482 |
. . 3
UMGraph
|
5 | | simpr3 1069 |
. . 3
UMGraph
|
6 | | s3wwlks2on.v |
. . . 4
Vtx |
7 | 6 | s3wwlks2on 26849 |
. . 3
UPGraph
WWalksNOn
Walks |
8 | 2, 4, 5, 7 | syl3anc 1326 |
. 2
UMGraph
WWalksNOn Walks |
9 | | eqid 2622 |
. . . . . . . 8
iEdg iEdg |
10 | 6, 9 | upgr2wlk 26564 |
. . . . . . 7
UPGraph Walks
..^
iEdg
iEdg iEdg |
11 | 1, 10 | syl 17 |
. . . . . 6
UMGraph Walks
..^
iEdg
iEdg iEdg |
12 | 11 | adantr 481 |
. . . . 5
UMGraph
Walks
..^
iEdg
iEdg iEdg |
13 | | s3fv0 13636 |
. . . . . . . . . . . 12
|
14 | 13 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
15 | | s3fv1 13637 |
. . . . . . . . . . . 12
|
16 | 15 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
17 | 14, 16 | preq12d 4276 |
. . . . . . . . . 10
|
18 | 17 | eqeq2d 2632 |
. . . . . . . . 9
iEdg
iEdg |
19 | | s3fv2 13638 |
. . . . . . . . . . . 12
|
20 | 19 | 3ad2ant3 1084 |
. . . . . . . . . . 11
|
21 | 16, 20 | preq12d 4276 |
. . . . . . . . . 10
|
22 | 21 | eqeq2d 2632 |
. . . . . . . . 9
iEdg
iEdg |
23 | 18, 22 | anbi12d 747 |
. . . . . . . 8
iEdg iEdg
iEdg
iEdg |
24 | 23 | adantl 482 |
. . . . . . 7
UMGraph
iEdg iEdg
iEdg
iEdg |
25 | 24 | 3anbi3d 1405 |
. . . . . 6
UMGraph
..^ iEdg iEdg iEdg ..^ iEdg iEdg
iEdg
|
26 | | umgruhgr 25999 |
. . . . . . . . . . 11
UMGraph UHGraph |
27 | 9 | uhgrfun 25961 |
. . . . . . . . . . 11
UHGraph
iEdg |
28 | | fdmrn 6064 |
. . . . . . . . . . . 12
iEdg iEdg iEdg iEdg |
29 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
..^ iEdg iEdg iEdg iEdg
iEdg iEdg iEdg |
30 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
..^
iEdg
..^ iEdg |
31 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | 31 | prid1 4297 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | | fzo0to2pr 12553 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
34 | 32, 33 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
..^
iEdg
..^ |
36 | 30, 35 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
..^
iEdg
iEdg |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ iEdg iEdg iEdg iEdg
iEdg |
38 | 29, 37 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^ iEdg iEdg iEdg iEdg
iEdg iEdg |
39 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . . . . . 22
|
40 | 39 | prid2 4298 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40, 33 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
..^
iEdg
..^ |
43 | 30, 42 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
..^
iEdg
iEdg |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ iEdg iEdg iEdg iEdg
iEdg |
45 | 29, 44 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
..^ iEdg iEdg iEdg iEdg
iEdg iEdg |
46 | 38, 45 | jca 554 |
. . . . . . . . . . . . . . 15
..^ iEdg iEdg iEdg iEdg
iEdg iEdg iEdg iEdg |
47 | 46 | ex 450 |
. . . . . . . . . . . . . 14
..^
iEdg
iEdg iEdg iEdg iEdg iEdg iEdg iEdg |
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
..^ iEdg iEdg iEdg
iEdg iEdg
iEdg
iEdg iEdg iEdg iEdg |
49 | 48 | com12 32 |
. . . . . . . . . . . 12
iEdg iEdg iEdg ..^ iEdg
iEdg
iEdg
iEdg iEdg iEdg iEdg |
50 | 28, 49 | sylbi 207 |
. . . . . . . . . . 11
iEdg ..^ iEdg
iEdg
iEdg
iEdg iEdg iEdg iEdg |
51 | 26, 27, 50 | 3syl 18 |
. . . . . . . . . 10
UMGraph ..^
iEdg
iEdg
iEdg
iEdg iEdg iEdg iEdg |
52 | 51 | imp 445 |
. . . . . . . . 9
UMGraph
..^ iEdg iEdg iEdg
iEdg iEdg iEdg iEdg |
53 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
iEdg
iEdg |
54 | 53 | biimpi 206 |
. . . . . . . . . . . . . 14
iEdg
iEdg |
55 | 54 | adantr 481 |
. . . . . . . . . . . . 13
iEdg
iEdg
iEdg |
56 | 55 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
..^ iEdg iEdg iEdg
iEdg |
57 | 56 | adantl 482 |
. . . . . . . . . . 11
UMGraph
..^ iEdg iEdg iEdg
iEdg |
58 | | usgrwwlks2on.e |
. . . . . . . . . . . . 13
Edg |
59 | | edgval 25941 |
. . . . . . . . . . . . 13
Edg iEdg |
60 | 58, 59 | eqtri 2644 |
. . . . . . . . . . . 12
iEdg |
61 | 60 | a1i 11 |
. . . . . . . . . . 11
UMGraph
..^ iEdg iEdg iEdg
iEdg |
62 | 57, 61 | eleq12d 2695 |
. . . . . . . . . 10
UMGraph
..^ iEdg iEdg iEdg
iEdg iEdg |
63 | | eqcom 2629 |
. . . . . . . . . . . . . . 15
iEdg
iEdg |
64 | 63 | biimpi 206 |
. . . . . . . . . . . . . 14
iEdg
iEdg |
65 | 64 | adantl 482 |
. . . . . . . . . . . . 13
iEdg
iEdg
iEdg |
66 | 65 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
..^ iEdg iEdg iEdg
iEdg |
67 | 66 | adantl 482 |
. . . . . . . . . . 11
UMGraph
..^ iEdg iEdg iEdg
iEdg |
68 | 67, 61 | eleq12d 2695 |
. . . . . . . . . 10
UMGraph
..^ iEdg iEdg iEdg
iEdg iEdg |
69 | 62, 68 | anbi12d 747 |
. . . . . . . . 9
UMGraph
..^ iEdg iEdg iEdg
iEdg iEdg iEdg iEdg |
70 | 52, 69 | mpbird 247 |
. . . . . . . 8
UMGraph
..^ iEdg iEdg iEdg
|
71 | 70 | ex 450 |
. . . . . . 7
UMGraph ..^
iEdg
iEdg
iEdg
|
72 | 71 | adantr 481 |
. . . . . 6
UMGraph
..^ iEdg iEdg iEdg
|
73 | 25, 72 | sylbid 230 |
. . . . 5
UMGraph
..^ iEdg iEdg iEdg
|
74 | 12, 73 | sylbid 230 |
. . . 4
UMGraph
Walks
|
75 | 74 | exlimdv 1861 |
. . 3
UMGraph
Walks
|
76 | 58 | umgr2wlk 26845 |
. . . . . . 7
UMGraph
Walks
|
77 | | wlklenvp1 26514 |
. . . . . . . . . . . . . . . . . . . 20
Walks
|
78 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
79 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . . . . . 22
|
80 | 78, 79 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . 21
|
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | 77, 81 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . 19
Walks
|
83 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
84 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
85 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
86 | 83, 84, 85 | 3anbi123i 1251 |
. . . . . . . . . . . . . . . . . . . . . 22
|
87 | 86 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
Walks
|
90 | 82, 89 | jca 554 |
. . . . . . . . . . . . . . . . . 18
Walks
|
91 | 6 | wlkpwrd 26513 |
. . . . . . . . . . . . . . . . . . . . 21
Walks
Word |
92 | 80 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
|
94 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
Word |
95 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ ..^ |
96 | | fzo0to3tp 12554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ |
97 | 95, 96 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ |
98 | 31 | tpid1 4303 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
99 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
100 | 98, 99 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^ |
101 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Word
..^ |
102 | 100, 101 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Word ..^ |
103 | 39 | tpid2 4304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
104 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
105 | 103, 104 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^ |
106 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Word
..^ |
107 | 105, 106 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Word ..^ |
108 | | 2ex 11092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
109 | 108 | tpid3 4307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
110 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
..^ ..^
|
111 | 109, 110 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
..^ ..^ |
112 | | wrdsymbcl 13318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
Word
..^ |
113 | 111, 112 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
Word ..^ |
114 | 102, 107,
113 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
Word ..^ |
115 | 97, 114 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Word |
116 | 115 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
|
117 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
118 | 117 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
119 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
120 | 119 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
121 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
122 | 121 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
123 | 118, 120,
122 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
124 | 123 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Word
|
125 | 116, 124 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Word
|
126 | 94, 125 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Word
Word
|
127 | 126 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Word
Word
|
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Word
Word
|
129 | 93, 128 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . 23
Word
Word
|
130 | 129 | impancom 456 |
. . . . . . . . . . . . . . . . . . . . . 22
Word
Word
|
131 | 130 | impd 447 |
. . . . . . . . . . . . . . . . . . . . 21
Word Word
|
132 | 91, 77, 131 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
Walks
Word
|
133 | 132 | imp 445 |
. . . . . . . . . . . . . . . . . . 19
Walks
Word
|
134 | | eqwrds3 13704 |
. . . . . . . . . . . . . . . . . . 19
Word
|
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Walks
|
136 | 90, 135 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
Walks
|
137 | 136 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
Walks
Walks
Walks |
138 | 137 | biimpd 219 |
. . . . . . . . . . . . . . 15
Walks
Walks Walks |
139 | 138 | ex 450 |
. . . . . . . . . . . . . 14
Walks
Walks
Walks |
140 | 139 | pm2.43a 54 |
. . . . . . . . . . . . 13
Walks
Walks |
141 | 140 | 3impib 1262 |
. . . . . . . . . . . 12
Walks Walks |
142 | 141 | adantl 482 |
. . . . . . . . . . 11
Walks
Walks |
143 | | simpr2 1068 |
. . . . . . . . . . 11
Walks
|
144 | 142, 143 | jca 554 |
. . . . . . . . . 10
Walks
Walks |
145 | 144 | ex 450 |
. . . . . . . . 9
Walks
Walks |
146 | 145 | exlimdv 1861 |
. . . . . . . 8
Walks Walks |
147 | 146 | eximdv 1846 |
. . . . . . 7
Walks
Walks |
148 | 76, 147 | syl5com 31 |
. . . . . 6
UMGraph
Walks |
149 | 148 | 3expib 1268 |
. . . . 5
UMGraph
Walks |
150 | 149 | com23 86 |
. . . 4
UMGraph
Walks |
151 | 150 | imp 445 |
. . 3
UMGraph
Walks |
152 | 75, 151 | impbid 202 |
. 2
UMGraph
Walks
|
153 | 8, 152 | bitrd 268 |
1
UMGraph
WWalksNOn
|