Metamath Proof Explorer

Theorem umgr2cwwkdifex

Description: If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Assertion umgr2cwwkdifex 
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> E. i e. ( 0 ..^ N ) ( W ` i ) =/= ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
2 1nn0 
 |-  1 e. NN0
3 2 a1i 
 |-  ( ( N e. NN /\ 1 < N ) -> 1 e. NN0 )
4 simpl 
 |-  ( ( N e. NN /\ 1 < N ) -> N e. NN )
5 simpr 
 |-  ( ( N e. NN /\ 1 < N ) -> 1 < N )
6 elfzo0 
 |-  ( 1 e. ( 0 ..^ N ) <-> ( 1 e. NN0 /\ N e. NN /\ 1 < N ) )
7 3 4 5 6 syl3anbrc 
 |-  ( ( N e. NN /\ 1 < N ) -> 1 e. ( 0 ..^ N ) )
8 1 7 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. ( 0 ..^ N ) )
9 8 3ad2ant2 
 |-  ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> 1 e. ( 0 ..^ N ) )
10 fveq2 
 |-  ( i = 1 -> ( W ` i ) = ( W ` 1 ) )
11 10 adantl 
 |-  ( ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) /\ i = 1 ) -> ( W ` i ) = ( W ` 1 ) )
12 11 neeq1d 
 |-  ( ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) /\ i = 1 ) -> ( ( W ` i ) =/= ( W ` 0 ) <-> ( W ` 1 ) =/= ( W ` 0 ) ) )
13 umgr2cwwk2dif 
 |-  ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )
14 9 12 13 rspcedvd 
 |-  ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> E. i e. ( 0 ..^ N ) ( W ` i ) =/= ( W ` 0 ) )