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	⊢ EulerPaths = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceupth	⊢ EulerPaths
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		vp	⊢ 𝑝
5	3	cv	⊢ 𝑓
6		ctrls	⊢ Trails
7	1	cv	⊢ 𝑔
8	7 6	cfv	⊢ ( Trails ‘ 𝑔 )
9	4	cv	⊢ 𝑝
10	5 9 8	wbr	⊢ 𝑓 ( Trails ‘ 𝑔 ) 𝑝
11		cc0	⊢ 0
12		cfzo	⊢ ..^
13		chash	⊢ ♯
14	5 13	cfv	⊢ ( ♯ ‘ 𝑓 )
15	11 14 12	co	⊢ ( 0 ..^ ( ♯ ‘ 𝑓 ) )
16		ciedg	⊢ iEdg
17	7 16	cfv	⊢ ( iEdg ‘ 𝑔 )
18	17	cdm	⊢ dom ( iEdg ‘ 𝑔 )
19	15 18 5	wfo	⊢ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 )
20	10 19	wa	⊢ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 ) )
21	20 3 4	copab	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 ) ) }
22	1 2 21	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 ) ) } )
23	0 22	wceq	⊢ EulerPaths = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ 𝑓 : ( 0 ..^ ( ♯ ‘ 𝑓 ) ) –onto→ dom ( iEdg ‘ 𝑔 ) ) } )