Metamath Proof Explorer


Theorem wlkv0

Description: If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion wlkv0
|- ( ( ( Vtx ` G ) = (/) /\ W e. ( Walks ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )

Proof

Step Hyp Ref Expression
1 wlkcpr
 |-  ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) )
2 eqid
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 2 wlkf
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 1st ` W ) e. Word dom ( iEdg ` G ) )
4 eqid
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 wlkp
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) )
6 3 5 jca
 |-  ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) )
7 feq3
 |-  ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) <-> ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> (/) ) )
8 f00
 |-  ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> (/) <-> ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) )
9 7 8 bitrdi
 |-  ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) <-> ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) ) )
10 0z
 |-  0 e. ZZ
11 nn0z
 |-  ( ( # ` ( 1st ` W ) ) e. NN0 -> ( # ` ( 1st ` W ) ) e. ZZ )
12 fzn
 |-  ( ( 0 e. ZZ /\ ( # ` ( 1st ` W ) ) e. ZZ ) -> ( ( # ` ( 1st ` W ) ) < 0 <-> ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) )
13 10 11 12 sylancr
 |-  ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( # ` ( 1st ` W ) ) < 0 <-> ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) )
14 nn0nlt0
 |-  ( ( # ` ( 1st ` W ) ) e. NN0 -> -. ( # ` ( 1st ` W ) ) < 0 )
15 14 pm2.21d
 |-  ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( # ` ( 1st ` W ) ) < 0 -> ( 1st ` W ) = (/) ) )
16 13 15 sylbird
 |-  ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) -> ( 1st ` W ) = (/) ) )
17 16 com12
 |-  ( ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) -> ( ( # ` ( 1st ` W ) ) e. NN0 -> ( 1st ` W ) = (/) ) )
18 17 adantl
 |-  ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) -> ( ( # ` ( 1st ` W ) ) e. NN0 -> ( 1st ` W ) = (/) ) )
19 lencl
 |-  ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( # ` ( 1st ` W ) ) e. NN0 )
20 18 19 impel
 |-  ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( 1st ` W ) = (/) )
21 simpll
 |-  ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( 2nd ` W ) = (/) )
22 20 21 jca
 |-  ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )
23 22 ex
 |-  ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) )
24 9 23 syl6bi
 |-  ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) )
25 24 impcomd
 |-  ( ( Vtx ` G ) = (/) -> ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) )
26 6 25 syl5
 |-  ( ( Vtx ` G ) = (/) -> ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) )
27 1 26 syl5bi
 |-  ( ( Vtx ` G ) = (/) -> ( W e. ( Walks ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) )
28 27 imp
 |-  ( ( ( Vtx ` G ) = (/) /\ W e. ( Walks ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )