Theorem iseupth

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	iseupth	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		eupths.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2	1	eupths	⊢ ( EulerPaths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom 𝐼 ) }
3		simpl	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑓 = 𝐹 )
4		fveq2	⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
5	4	oveq2d	⊢ ( 𝑓 = 𝐹 → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6	5	adantr	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 0 ..^ ( ♯ ‘ 𝑓 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
7		eqidd	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → dom 𝐼 = dom 𝐼 )
8	3 6 7	foeq123d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) )
9		reltrls	⊢ Rel ( Trails ‘ 𝐺 )
10	2 8 9	brfvopabrbr	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 ) )