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 ) = (/) )