Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eupa Structured version   Unicode version

Definition df-eupa 24786
 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 UMGrph
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-eupa
StepHypRef Expression
1 ceup 24785 . 2 EulPaths
2 vv . . 3
3 ve . . 3
4 cvv 3118 . . 3
52cv 1378 . . . . . 6
63cv 1378 . . . . . 6
7 cumg 24135 . . . . . 6 UMGrph
85, 6, 7wbr 4453 . . . . 5 UMGrph
9 c1 9505 . . . . . . . . 9
10 vn . . . . . . . . . 10
1110cv 1378 . . . . . . . . 9
12 cfz 11684 . . . . . . . . 9
139, 11, 12co 6295 . . . . . . . 8
146cdm 5005 . . . . . . . 8
15 vf . . . . . . . . 9
1615cv 1378 . . . . . . . 8
1713, 14, 16wf1o 5593 . . . . . . 7
18 cc0 9504 . . . . . . . . 9
1918, 11, 12co 6295 . . . . . . . 8
20 vp . . . . . . . . 9
2120cv 1378 . . . . . . . 8
2219, 5, 21wf 5590 . . . . . . 7
23 vk . . . . . . . . . . . 12
2423cv 1378 . . . . . . . . . . 11
2524, 16cfv 5594 . . . . . . . . . 10
2625, 6cfv 5594 . . . . . . . . 9
27 cmin 9817 . . . . . . . . . . . 12
2824, 9, 27co 6295 . . . . . . . . . . 11
2928, 21cfv 5594 . . . . . . . . . 10
3024, 21cfv 5594 . . . . . . . . . 10
3129, 30cpr 4035 . . . . . . . . 9
3226, 31wceq 1379 . . . . . . . 8
3332, 23, 13wral 2817 . . . . . . 7
3417, 22, 33w3a 973 . . . . . 6
35 cn0 10807 . . . . . 6
3634, 10, 35wrex 2818 . . . . 5
378, 36wa 369 . . . 4 UMGrph
3837, 15, 20copab 4510 . . 3 UMGrph
392, 3, 4, 4, 38cmpt2 6297 . 2 UMGrph
401, 39wceq 1379 1 EulPaths UMGrph
 Colors of variables: wff setvar class This definition is referenced by:  releupa  24787  iseupa  24788  eupatrl  24791
 Copyright terms: Public domain W3C validator