Step |
Hyp |
Ref |
Expression |
1 |
|
wlkn0 |
⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ≠ ∅ ) |
2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
3 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
4 |
2 3
|
upgriswlk |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ) |
5 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ≠ ∅ ) |
6 |
|
ffz0iswrd |
⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) |
7 |
6
|
3ad2ant2 |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) |
8 |
7
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ) |
9 |
|
upgruhgr |
⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph ) |
10 |
3
|
uhgrfun |
⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) ) |
11 |
|
funfn |
⊢ ( Fun ( iEdg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ) |
12 |
11
|
biimpi |
⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ) |
13 |
9 10 12
|
3syl |
⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ) |
14 |
13
|
ad2antlr |
⊢ ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ) |
15 |
|
wrdsymbcl |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) ) |
16 |
15
|
ad4ant14 |
⊢ ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) ) |
17 |
|
fnfvelrn |
⊢ ( ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ∧ ( 𝐹 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) |
18 |
14 16 17
|
syl2anc |
⊢ ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ran ( iEdg ‘ 𝐺 ) ) |
19 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
20 |
18 19
|
eleqtrrdi |
⊢ ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) |
21 |
|
eleq1 |
⊢ ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) |
22 |
21
|
eqcoms |
⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) |
23 |
20 22
|
syl5ibrcom |
⊢ ( ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
24 |
23
|
ralimdva |
⊢ ( ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) ∧ 𝐺 ∈ UPGraph ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
25 |
24
|
ex |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ∈ UPGraph → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
26 |
25
|
com23 |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) |
27 |
26
|
3impia |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝐺 ∈ UPGraph → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
28 |
27
|
impcom |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
29 |
|
lencl |
⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) |
30 |
|
ffz0hash |
⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) |
31 |
30
|
ex |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) ) |
32 |
|
oveq1 |
⊢ ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) ) |
33 |
|
nn0cn |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ ) |
34 |
|
pncan1 |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) |
35 |
33 34
|
syl |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ( ♯ ‘ 𝐹 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) |
36 |
32 35
|
sylan9eqr |
⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) |
37 |
36
|
ex |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) ) |
38 |
31 37
|
syld |
⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) ) |
39 |
29 38
|
syl |
⊢ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) ) |
40 |
39
|
imp |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) = ( ♯ ‘ 𝐹 ) ) |
41 |
40
|
oveq2d |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) |
42 |
41
|
raleqdv |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
43 |
42
|
3adant3 |
⊢ ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
44 |
43
|
adantl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
45 |
28 44
|
mpbird |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
46 |
45
|
adantr |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) |
47 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
48 |
2 47
|
iswwlks |
⊢ ( 𝑃 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑃 ≠ ∅ ∧ 𝑃 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
49 |
5 8 46 48
|
syl3anbrc |
⊢ ( ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) ∧ 𝑃 ≠ ∅ ) → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) |
50 |
49
|
ex |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) |
51 |
50
|
ex |
⊢ ( 𝐺 ∈ UPGraph → ( ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) ) |
52 |
4 51
|
sylbid |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ≠ ∅ → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) ) |
53 |
1 52
|
mpdi |
⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 ∈ ( WWalks ‘ 𝐺 ) ) ) |