Step |
Hyp |
Ref |
Expression |
1 |
|
eupth0.v |
|- V = ( Vtx ` G ) |
2 |
|
eupth0.i |
|- I = ( iEdg ` G ) |
3 |
|
eqidd |
|- ( A e. V -> { <. 0 , A >. } = { <. 0 , A >. } ) |
4 |
1
|
is0wlk |
|- ( ( { <. 0 , A >. } = { <. 0 , A >. } /\ A e. V ) -> (/) ( Walks ` G ) { <. 0 , A >. } ) |
5 |
3 4
|
mpancom |
|- ( A e. V -> (/) ( Walks ` G ) { <. 0 , A >. } ) |
6 |
|
f1o0 |
|- (/) : (/) -1-1-onto-> (/) |
7 |
|
eqidd |
|- ( I = (/) -> (/) = (/) ) |
8 |
|
hash0 |
|- ( # ` (/) ) = 0 |
9 |
8
|
oveq2i |
|- ( 0 ..^ ( # ` (/) ) ) = ( 0 ..^ 0 ) |
10 |
|
fzo0 |
|- ( 0 ..^ 0 ) = (/) |
11 |
9 10
|
eqtri |
|- ( 0 ..^ ( # ` (/) ) ) = (/) |
12 |
11
|
a1i |
|- ( I = (/) -> ( 0 ..^ ( # ` (/) ) ) = (/) ) |
13 |
|
dmeq |
|- ( I = (/) -> dom I = dom (/) ) |
14 |
|
dm0 |
|- dom (/) = (/) |
15 |
13 14
|
eqtrdi |
|- ( I = (/) -> dom I = (/) ) |
16 |
7 12 15
|
f1oeq123d |
|- ( I = (/) -> ( (/) : ( 0 ..^ ( # ` (/) ) ) -1-1-onto-> dom I <-> (/) : (/) -1-1-onto-> (/) ) ) |
17 |
6 16
|
mpbiri |
|- ( I = (/) -> (/) : ( 0 ..^ ( # ` (/) ) ) -1-1-onto-> dom I ) |
18 |
5 17
|
anim12i |
|- ( ( A e. V /\ I = (/) ) -> ( (/) ( Walks ` G ) { <. 0 , A >. } /\ (/) : ( 0 ..^ ( # ` (/) ) ) -1-1-onto-> dom I ) ) |
19 |
2
|
iseupthf1o |
|- ( (/) ( EulerPaths ` G ) { <. 0 , A >. } <-> ( (/) ( Walks ` G ) { <. 0 , A >. } /\ (/) : ( 0 ..^ ( # ` (/) ) ) -1-1-onto-> dom I ) ) |
20 |
18 19
|
sylibr |
|- ( ( A e. V /\ I = (/) ) -> (/) ( EulerPaths ` G ) { <. 0 , A >. } ) |