Step |
Hyp |
Ref |
Expression |
1 |
|
eupths.i |
|- I = ( iEdg ` G ) |
2 |
1
|
iseupth |
|- ( F ( EulerPaths ` G ) P <-> ( F ( Trails ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) ) |
3 |
|
istrl |
|- ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) ) |
4 |
3
|
anbi1i |
|- ( ( F ( Trails ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) <-> ( ( F ( Walks ` G ) P /\ Fun `' F ) /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) ) |
5 |
|
anass |
|- ( ( ( F ( Walks ` G ) P /\ Fun `' F ) /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) <-> ( F ( Walks ` G ) P /\ ( Fun `' F /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) ) ) |
6 |
|
ancom |
|- ( ( Fun `' F /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) <-> ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) ) |
7 |
6
|
anbi2i |
|- ( ( F ( Walks ` G ) P /\ ( Fun `' F /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) ) <-> ( F ( Walks ` G ) P /\ ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) ) ) |
8 |
4 5 7
|
3bitri |
|- ( ( F ( Trails ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) <-> ( F ( Walks ` G ) P /\ ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) ) ) |
9 |
|
dff1o3 |
|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) ) |
10 |
9
|
bicomi |
|- ( ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) <-> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) |
11 |
10
|
anbi2i |
|- ( ( F ( Walks ` G ) P /\ ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I /\ Fun `' F ) ) <-> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) ) |
12 |
2 8 11
|
3bitri |
|- ( F ( EulerPaths ` G ) P <-> ( F ( Walks ` G ) P /\ F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I ) ) |