Metamath Proof Explorer

Theorem 0enwwlksnge1

Description: In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018) (Revised by AV, 7-May-2021)

Ref Expression
Assertion 0enwwlksnge1 
|- ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( N WWalksN G ) = (/) )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
2 wwlksn 
 |-  ( N e. NN0 -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
3 1 2 syl 
 |-  ( N e. NN -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
4 3 adantl 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( N WWalksN G ) = { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
7 5 6 iswwlks 
 |-  ( w e. ( WWalks ` G ) <-> ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) )
8 nncn 
 |-  ( N e. NN -> N e. CC )
9 pncan1 
 |-  ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
10 8 9 syl 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
11 id 
 |-  ( N e. NN -> N e. NN )
12 10 11 eqeltrd 
 |-  ( N e. NN -> ( ( N + 1 ) - 1 ) e. NN )
13 12 adantl 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( ( N + 1 ) - 1 ) e. NN )
14 13 adantl 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( ( N + 1 ) - 1 ) e. NN )
15 oveq1 
 |-  ( ( # ` w ) = ( N + 1 ) -> ( ( # ` w ) - 1 ) = ( ( N + 1 ) - 1 ) )
16 15 eleq1d 
 |-  ( ( # ` w ) = ( N + 1 ) -> ( ( ( # ` w ) - 1 ) e. NN <-> ( ( N + 1 ) - 1 ) e. NN ) )
17 16 adantr 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( ( ( # ` w ) - 1 ) e. NN <-> ( ( N + 1 ) - 1 ) e. NN ) )
18 14 17 mpbird 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( ( # ` w ) - 1 ) e. NN )
19 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( ( # ` w ) - 1 ) ) <-> ( ( # ` w ) - 1 ) e. NN )
20 18 19 sylibr 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> 0 e. ( 0 ..^ ( ( # ` w ) - 1 ) ) )
21 fveq2 
 |-  ( i = 0 -> ( w ` i ) = ( w ` 0 ) )
22 fv0p1e1 
 |-  ( i = 0 -> ( w ` ( i + 1 ) ) = ( w ` 1 ) )
23 21 22 preq12d 
 |-  ( i = 0 -> { ( w ` i ) , ( w ` ( i + 1 ) ) } = { ( w ` 0 ) , ( w ` 1 ) } )
24 23 eleq1d 
 |-  ( i = 0 -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
25 24 adantl 
 |-  ( ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) /\ i = 0 ) -> ( { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
26 20 25 rspcdv 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) ) )
27 eleq2 
 |-  ( ( Edg ` G ) = (/) -> ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) <-> { ( w ` 0 ) , ( w ` 1 ) } e. (/) ) )
28 noel 
 |-  -. { ( w ` 0 ) , ( w ` 1 ) } e. (/)
29 28 pm2.21i 
 |-  ( { ( w ` 0 ) , ( w ` 1 ) } e. (/) -> -. ( # ` w ) = ( N + 1 ) )
30 27 29 biimtrdi 
 |-  ( ( Edg ` G ) = (/) -> ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) -> -. ( # ` w ) = ( N + 1 ) ) )
31 30 adantr 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) -> -. ( # ` w ) = ( N + 1 ) ) )
32 31 adantl 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( { ( w ` 0 ) , ( w ` 1 ) } e. ( Edg ` G ) -> -. ( # ` w ) = ( N + 1 ) ) )
33 26 32 syldc 
 |-  ( A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> -. ( # ` w ) = ( N + 1 ) ) )
34 33 3ad2ant3 
 |-  ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> -. ( # ` w ) = ( N + 1 ) ) )
35 34 com12 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( ( w =/= (/) /\ w e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. ( Edg ` G ) ) -> -. ( # ` w ) = ( N + 1 ) ) )
36 7 35 biimtrid 
 |-  ( ( ( # ` w ) = ( N + 1 ) /\ ( ( Edg ` G ) = (/) /\ N e. NN ) ) -> ( w e. ( WWalks ` G ) -> -. ( # ` w ) = ( N + 1 ) ) )
37 36 expimpd 
 |-  ( ( # ` w ) = ( N + 1 ) -> ( ( ( ( Edg ` G ) = (/) /\ N e. NN ) /\ w e. ( WWalks ` G ) ) -> -. ( # ` w ) = ( N + 1 ) ) )
38 ax-1 
 |-  ( -. ( # ` w ) = ( N + 1 ) -> ( ( ( ( Edg ` G ) = (/) /\ N e. NN ) /\ w e. ( WWalks ` G ) ) -> -. ( # ` w ) = ( N + 1 ) ) )
39 37 38 pm2.61i 
 |-  ( ( ( ( Edg ` G ) = (/) /\ N e. NN ) /\ w e. ( WWalks ` G ) ) -> -. ( # ` w ) = ( N + 1 ) )
40 39 ralrimiva 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> A. w e. ( WWalks ` G ) -. ( # ` w ) = ( N + 1 ) )
41 rabeq0 
 |-  ( { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = (/) <-> A. w e. ( WWalks ` G ) -. ( # ` w ) = ( N + 1 ) )
42 40 41 sylibr 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> { w e. ( WWalks ` G ) | ( # ` w ) = ( N + 1 ) } = (/) )
43 4 42 eqtrd 
 |-  ( ( ( Edg ` G ) = (/) /\ N e. NN ) -> ( N WWalksN G ) = (/) )