Metamath Proof Explorer

Theorem upgriseupth

Description: The property " <. F , P >. is an Eulerian path on the pseudograph G ". (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)

Ref Expression
Hypotheses eupths.i 
|- I = ( iEdg ` G )
upgriseupth.v 
|- V = ( Vtx ` G )
Assertion upgriseupth 
|- ( G e. UPGraph -> ( F ( EulerPaths ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )

Proof

Step Hyp Ref Expression
1 eupths.i 
 |-  I = ( iEdg ` G )
2 upgriseupth.v 
 |-  V = ( Vtx ` G )
3 1 iseupthf1o 
 |-  ( F ( EulerPaths ` G ) P <-> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) )
4 3 a1i 
 |-  ( G e. UPGraph -> ( F ( EulerPaths ` G ) P <-> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) ) )
5 2 1 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
6 5 anbi1d 
 |-  ( G e. UPGraph -> ( ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) ) )
7 simpr 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
8 simpl2 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) -> P : ( 0 ... ( # ` F ) ) --> V )
9 simpl3 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
10 7 8 9 3jca 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
11 f1of 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
12 iswrdi 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F e. Word dom I )
13 11 12 syl 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> F e. Word dom I )
14 13 3anim1i 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
15 simp1 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
16 14 15 jca 
 |-  ( ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) )
17 10 16 impbii 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) )
18 17 a1i 
 |-  ( G e. UPGraph -> ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
19 4 6 18 3bitrd 
 |-  ( G e. UPGraph -> ( F ( EulerPaths ` G ) P <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )