Definition df-eupth

Description: Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

	Ref	Expression
Assertion	df-eupth	$$⊢\mathrm{EulerPaths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge f:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceupth	$$class\mathrm{EulerPaths}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		vp	$$setvarp$$
5	3	cv	$$setvarf$$
6		ctrls	$$class\mathrm{Trails}$$
7	1	cv	$$setvarg$$
8	7 6	cfv	$$class\mathrm{Trails}\left(g\right)$$
9	4	cv	$$setvarp$$
10	5 9 8	wbr	$$wfff\mathrm{Trails}\left(g\right)p$$
11		cc0	$$class0$$
12		cfzo	$$class..^$$
13		chash	$$class\left|.\right|$$
14	5 13	cfv	$$class\left|f\right|$$
15	11 14 12	co	$$class\left(0..^\left|f\right|\right)$$
16		ciedg	$$class\mathrm{iEdg}$$
17	7 16	cfv	$$class\mathrm{iEdg}\left(g\right)$$
18	17	cdm	$$class\mathrm{dom}\mathrm{iEdg}\left(g\right)$$
19	15 18 5	wfo	$$wfff:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)$$
20	10 19	wa	$$wff\left(f\mathrm{Trails}\left(g\right)p\wedge f:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)\right)$$
21	20 3 4	copab	$$class\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge f:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)\right)\right\}$$
22	1 2 21	cmpt	$$class\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge f:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)\right)\right\}\right)$$
23	0 22	wceq	$$wff\mathrm{EulerPaths}=\left(g\in \mathrm{V}⟼\left\{⟨f,p⟩|\left(f\mathrm{Trails}\left(g\right)p\wedge f:\left(0..^\left|f\right|\right)\underset{onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(g\right)\right)\right\}\right)$$