Step |
Hyp |
Ref |
Expression |
1 |
|
eupths.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
2 |
1
|
iseupth |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ) |
3 |
|
istrl |
⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) ) |
4 |
3
|
anbi1i |
⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ↔ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ) |
5 |
|
anass |
⊢ ( ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ 𝐹 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ) ) |
6 |
|
ancom |
⊢ ( ( Fun ◡ 𝐹 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ) |
7 |
6
|
anbi2i |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ 𝐹 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ) ) |
8 |
4 5 7
|
3bitri |
⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ) ) |
9 |
|
dff1o3 |
⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ↔ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ) |
10 |
9
|
bicomi |
⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) |
11 |
10
|
anbi2i |
⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ∧ Fun ◡ 𝐹 ) ) ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) ) |
12 |
2 8 11
|
3bitri |
⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) ) |