This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem g0wlk0

Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion g0wlk0 
|- ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) )

Proof

Step Hyp Ref Expression
1 ax-1 
 |-  ( ( Walks ` G ) = (/) -> ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) )
2 neq0 
 |-  ( -. ( Walks ` G ) = (/) <-> E. w w e. ( Walks ` G ) )
3 wlkv0 
 |-  ( ( ( Vtx ` G ) = (/) /\ w e. ( Walks ` G ) ) -> ( ( 1st ` w ) = (/) /\ ( 2nd ` w ) = (/) ) )
4 wlkcpr 
 |-  ( w e. ( Walks ` G ) <-> ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) )
5 wlkn0 
 |-  ( ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) -> ( 2nd ` w ) =/= (/) )
6 eqneqall 
 |-  ( ( 2nd ` w ) = (/) -> ( ( 2nd ` w ) =/= (/) -> ( Walks ` G ) = (/) ) )
7 6 adantl 
 |-  ( ( ( 1st ` w ) = (/) /\ ( 2nd ` w ) = (/) ) -> ( ( 2nd ` w ) =/= (/) -> ( Walks ` G ) = (/) ) )
8 5 7 syl5com 
 |-  ( ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) -> ( ( ( 1st ` w ) = (/) /\ ( 2nd ` w ) = (/) ) -> ( Walks ` G ) = (/) ) )
9 4 8 sylbi 
 |-  ( w e. ( Walks ` G ) -> ( ( ( 1st ` w ) = (/) /\ ( 2nd ` w ) = (/) ) -> ( Walks ` G ) = (/) ) )
10 9 adantl 
 |-  ( ( ( Vtx ` G ) = (/) /\ w e. ( Walks ` G ) ) -> ( ( ( 1st ` w ) = (/) /\ ( 2nd ` w ) = (/) ) -> ( Walks ` G ) = (/) ) )
11 3 10 mpd 
 |-  ( ( ( Vtx ` G ) = (/) /\ w e. ( Walks ` G ) ) -> ( Walks ` G ) = (/) )
12 11 expcom 
 |-  ( w e. ( Walks ` G ) -> ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) )
13 12 exlimiv 
 |-  ( E. w w e. ( Walks ` G ) -> ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) )
14 2 13 sylbi 
 |-  ( -. ( Walks ` G ) = (/) -> ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) )
15 1 14 pm2.61i 
 |-  ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) )