This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑔 ) ) } )