Metamath Proof Explorer

Theorem iseupthf1o

Description: The property " <. F , P >. is an Eulerian path on the graph G ". An Eulerian path is defined as bijection F from the edges to a set 0 ... ( N - 1 ) and a function P : ( 0 ... N ) --> V into the vertices such that for each 0 <_ k < N , F ( k ) is an edge from P ( k ) to P ( k + 1 ) . (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 18-Feb-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis eupths.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion iseupthf1o ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) )

Proof

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 𝐼 ) )