Step |
Hyp |
Ref |
Expression |
1 |
|
upgreupthseg.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
3 |
1 2
|
upgreupthi |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑛 ) ) = { ( 𝑃 ‘ 𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) ) |
4 |
|
2fveq3 |
⊢ ( 𝑛 = 𝑁 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑛 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) |
5 |
|
fveq2 |
⊢ ( 𝑛 = 𝑁 → ( 𝑃 ‘ 𝑛 ) = ( 𝑃 ‘ 𝑁 ) ) |
6 |
|
fvoveq1 |
⊢ ( 𝑛 = 𝑁 → ( 𝑃 ‘ ( 𝑛 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) ) |
7 |
5 6
|
preq12d |
⊢ ( 𝑛 = 𝑁 → { ( 𝑃 ‘ 𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) |
8 |
4 7
|
eqeq12d |
⊢ ( 𝑛 = 𝑁 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝑛 ) ) = { ( 𝑃 ‘ 𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) |
9 |
8
|
rspccv |
⊢ ( ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑛 ) ) = { ( 𝑃 ‘ 𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) |
10 |
9
|
3ad2ant3 |
⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑛 ) ) = { ( 𝑃 ‘ 𝑛 ) , ( 𝑃 ‘ ( 𝑛 + 1 ) ) } ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) |
11 |
3 10
|
syl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) ) |
12 |
11
|
3impia |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ) |