Metamath Proof Explorer


Theorem eupth0

Description: There is an Eulerian path on an empty graph, i.e. a graph with at least one vertex, but without an edge. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 5-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Hypotheses eupth0.v
|- V = ( Vtx ` G )
eupth0.i
|- I = ( iEdg ` G )
Assertion eupth0
|- ( ( A e. V /\ I = (/) ) -> (/) ( EulerPaths ` G ) { <. 0 , A >. } )

Proof

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 >. } )