Step |
Hyp |
Ref |
Expression |
1 |
|
wlkiswwlks2lem.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) |
2 |
|
wlkiswwlks2lem.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
2
|
uspgrf1oedg |
⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) ) |
4 |
2
|
rneqi |
⊢ ran 𝐸 = ran ( iEdg ‘ 𝐺 ) |
5 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
6 |
4 5
|
eqtr4i |
⊢ ran 𝐸 = ( Edg ‘ 𝐺 ) |
7 |
6
|
a1i |
⊢ ( 𝐺 ∈ USPGraph → ran 𝐸 = ( Edg ‘ 𝐺 ) ) |
8 |
7
|
f1oeq3d |
⊢ ( 𝐺 ∈ USPGraph → ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ↔ 𝐸 : dom 𝐸 –1-1-onto→ ( Edg ‘ 𝐺 ) ) ) |
9 |
3 8
|
mpbird |
⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ) |
10 |
9
|
3ad2ant1 |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ) |
11 |
10
|
ad2antrr |
⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ) |
12 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) |
13 |
|
fveq2 |
⊢ ( 𝑖 = 𝑥 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑥 ) ) |
14 |
|
fvoveq1 |
⊢ ( 𝑖 = 𝑥 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑥 + 1 ) ) ) |
15 |
13 14
|
preq12d |
⊢ ( 𝑖 = 𝑥 → { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) |
16 |
15
|
eleq1d |
⊢ ( 𝑖 = 𝑥 → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) |
17 |
16
|
adantl |
⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) ∧ 𝑖 = 𝑥 ) → ( { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ↔ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) |
18 |
12 17
|
rspcdv |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) |
19 |
18
|
impancom |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) ) |
20 |
19
|
imp |
⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) |
21 |
|
f1ocnvdm |
⊢ ( ( 𝐸 : dom 𝐸 –1-1-onto→ ran 𝐸 ∧ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ∈ ran 𝐸 ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) |
22 |
11 20 21
|
syl2anc |
⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) ∧ 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ dom 𝐸 ) |
23 |
22 1
|
fmptd |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸 ) |
24 |
|
iswrdi |
⊢ ( 𝐹 : ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ⟶ dom 𝐸 → 𝐹 ∈ Word dom 𝐸 ) |
25 |
23 24
|
syl |
⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 ) → 𝐹 ∈ Word dom 𝐸 ) |
26 |
25
|
ex |
⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸 ) ) |