MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iseupthf1o Structured version   Visualization version   GIF version

Theorem iseupthf1o 29964
Description: The property "โŸจ๐น, ๐‘ƒโŸฉ is an Eulerian path on the graph ๐บ". An Eulerian path is defined as bijection ๐น from the edges to a set 0...(๐‘ โˆ’ 1) and a function ๐‘ƒ:(0...๐‘)โŸถ๐‘‰ into the vertices such that for each 0 โ‰ค ๐‘˜ < ๐‘, ๐น(๐‘˜) is an edge from ๐‘ƒ(๐‘˜) to ๐‘ƒ(๐‘˜ + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
Hypothesis
Ref Expression
eupths.i ๐ผ = (iEdgโ€˜๐บ)
Assertion
Ref Expression
iseupthf1o (๐น(EulerPathsโ€˜๐บ)๐‘ƒ โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“1-1-ontoโ†’dom ๐ผ))

Proof of Theorem iseupthf1o
StepHypRef Expression
1 eupths.i . . 3 ๐ผ = (iEdgโ€˜๐บ)
21iseupth 29963 . 2 (๐น(EulerPathsโ€˜๐บ)๐‘ƒ โ†” (๐น(Trailsโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ))
3 istrl 29462 . . . 4 (๐น(Trailsโ€˜๐บ)๐‘ƒ โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง Fun โ—ก๐น))
43anbi1i 623 . . 3 ((๐น(Trailsโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ) โ†” ((๐น(Walksโ€˜๐บ)๐‘ƒ โˆง Fun โ—ก๐น) โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ))
5 anass 468 . . 3 (((๐น(Walksโ€˜๐บ)๐‘ƒ โˆง Fun โ—ก๐น) โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ) โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง (Fun โ—ก๐น โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ)))
6 ancom 460 . . . 4 ((Fun โ—ก๐น โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ) โ†” (๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น))
76anbi2i 622 . . 3 ((๐น(Walksโ€˜๐บ)๐‘ƒ โˆง (Fun โ—ก๐น โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ)) โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง (๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น)))
84, 5, 73bitri 297 . 2 ((๐น(Trailsโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ) โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง (๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น)))
9 dff1o3 6833 . . . 4 (๐น:(0..^(โ™ฏโ€˜๐น))โ€“1-1-ontoโ†’dom ๐ผ โ†” (๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น))
109bicomi 223 . . 3 ((๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น) โ†” ๐น:(0..^(โ™ฏโ€˜๐น))โ€“1-1-ontoโ†’dom ๐ผ)
1110anbi2i 622 . 2 ((๐น(Walksโ€˜๐บ)๐‘ƒ โˆง (๐น:(0..^(โ™ฏโ€˜๐น))โ€“ontoโ†’dom ๐ผ โˆง Fun โ—ก๐น)) โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“1-1-ontoโ†’dom ๐ผ))
122, 8, 113bitri 297 1 (๐น(EulerPathsโ€˜๐บ)๐‘ƒ โ†” (๐น(Walksโ€˜๐บ)๐‘ƒ โˆง ๐น:(0..^(โ™ฏโ€˜๐น))โ€“1-1-ontoโ†’dom ๐ผ))
Colors of variables: wff setvar class
Syntax hints:   โ†” wb 205   โˆง wa 395   = wceq 1533   class class class wbr 5141  โ—กccnv 5668  dom cdm 5669  Fun wfun 6531  โ€“ontoโ†’wfo 6535  โ€“1-1-ontoโ†’wf1o 6536  โ€˜cfv 6537  (class class class)co 7405  0cc0 11112  ..^cfzo 13633  โ™ฏchash 14295  iEdgciedg 28765  Walkscwlks 29362  Trailsctrls 29456  EulerPathsceupth 29959
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7408  df-wlks 29365  df-trls 29458  df-eupth 29960
This theorem is referenced by:  eupthi  29965  upgriseupth  29969  eupth0  29976  eupthres  29977  eupthp1  29978
  Copyright terms: Public domain W3C validator