Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-eupa Unicode version

Definition df-eupa 23879
Description: Define the set of all Eulerian paths on an undirected multigraph. (Contributed by Mario Carneiro, 12-Mar-2015.)
Assertion
Ref Expression
df-eupa  |- EulPaths  =  ( v  e.  _V , 
e  e.  _V  |->  {
<. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n
) ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } )
Distinct variable group:    e, f, k, n, p, v

Detailed syntax breakdown of Definition df-eupa
StepHypRef Expression
1 ceup 23876 . 2  class EulPaths
2 vv . . 3  set  v
3 ve . . 3  set  e
4 cvv 2801 . . 3  class  _V
52cv 1631 . . . . . 6  class  v
63cv 1631 . . . . . 6  class  e
7 cumg 23875 . . . . . 6  class UMGrph
85, 6, 7wbr 4039 . . . . 5  wff  v UMGrph  e
9 c1 8754 . . . . . . . . 9  class  1
10 vn . . . . . . . . . 10  set  n
1110cv 1631 . . . . . . . . 9  class  n
12 cfz 10798 . . . . . . . . 9  class  ...
139, 11, 12co 5874 . . . . . . . 8  class  ( 1 ... n )
146cdm 4705 . . . . . . . 8  class  dom  e
15 vf . . . . . . . . 9  set  f
1615cv 1631 . . . . . . . 8  class  f
1713, 14, 16wf1o 5270 . . . . . . 7  wff  f : ( 1 ... n
)
-1-1-onto-> dom  e
18 cc0 8753 . . . . . . . . 9  class  0
1918, 11, 12co 5874 . . . . . . . 8  class  ( 0 ... n )
20 vp . . . . . . . . 9  set  p
2120cv 1631 . . . . . . . 8  class  p
2219, 5, 21wf 5267 . . . . . . 7  wff  p : ( 0 ... n
) --> v
23 vk . . . . . . . . . . . 12  set  k
2423cv 1631 . . . . . . . . . . 11  class  k
2524, 16cfv 5271 . . . . . . . . . 10  class  ( f `
 k )
2625, 6cfv 5271 . . . . . . . . 9  class  ( e `
 ( f `  k ) )
27 cmin 9053 . . . . . . . . . . . 12  class  -
2824, 9, 27co 5874 . . . . . . . . . . 11  class  ( k  -  1 )
2928, 21cfv 5271 . . . . . . . . . 10  class  ( p `
 ( k  - 
1 ) )
3024, 21cfv 5271 . . . . . . . . . 10  class  ( p `
 k )
3129, 30cpr 3654 . . . . . . . . 9  class  { ( p `  ( k  -  1 ) ) ,  ( p `  k ) }
3226, 31wceq 1632 . . . . . . . 8  wff  ( e `
 ( f `  k ) )  =  { ( p `  ( k  -  1 ) ) ,  ( p `  k ) }
3332, 23, 13wral 2556 . . . . . . 7  wff  A. k  e.  ( 1 ... n
) ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) }
3417, 22, 33w3a 934 . . . . . 6  wff  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } )
35 cn0 9981 . . . . . 6  class  NN0
3634, 10, 35wrex 2557 . . . . 5  wff  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } )
378, 36wa 358 . . . 4  wff  ( v UMGrph 
e  /\  E. n  e.  NN0  ( f : ( 1 ... n
)
-1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) )
3837, 15, 20copab 4092 . . 3  class  { <. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) }
392, 3, 4, 4, 38cmpt2 5876 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { <. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  ( f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n ) ( e `  ( f `
 k ) )  =  { ( p `
 ( k  - 
1 ) ) ,  ( p `  k
) } ) ) } )
401, 39wceq 1632 1  wff EulPaths  =  ( v  e.  _V , 
e  e.  _V  |->  {
<. f ,  p >.  |  ( v UMGrph  e  /\  E. n  e.  NN0  (
f : ( 1 ... n ) -1-1-onto-> dom  e  /\  p : ( 0 ... n ) --> v  /\  A. k  e.  ( 1 ... n
) ( e `  ( f `  k
) )  =  {
( p `  (
k  -  1 ) ) ,  ( p `
 k ) } ) ) } )
Colors of variables: wff set class
This definition is referenced by:  releupa  23895  iseupa  23896  eupatrl  28385
  Copyright terms: Public domain W3C validator