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