Theorem eupths

Description: The Eulerian paths on the graph G . (Contributed by AV, 18-Feb-2021) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Hypothesis	eupths.i	|- I = ( iEdg ` G )
Assertion	eupths	|- ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) }

Proof

Step	Hyp	Ref	Expression
1		eupths.i	|- I = ( iEdg ` G )
2		fveq2	|- ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
3	2 1	eqtr4di	|- ( g = G -> ( iEdg ` g ) = I )
4	3	dmeqd	|- ( g = G -> dom ( iEdg ` g ) = dom I )
5		foeq3	|- ( dom ( iEdg ` g ) = dom I -> ( f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) <-> f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) )
6	4 5	syl	|- ( g = G -> ( f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) <-> f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) )
7		df-eupth	|- EulerPaths = ( g e. _V |-> { <. f , p >. | ( f ( Trails ` g ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom ( iEdg ` g ) ) } )
8	6 7	fvmptopab	|- ( EulerPaths ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ f : ( 0 ..^ ( # ` f ) ) -onto-> dom I ) }