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