Metamath Proof Explorer

Theorem wwlksnextproplem1

Description: Lemma 1 for wwlksnextprop . (Contributed by Alexander van der Vekens, 31-Jul-2018) (Revised by AV, 20-Apr-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypothesis wwlksnextprop.x 
|- X = ( ( N + 1 ) WWalksN G )
Assertion wwlksnextproplem1 
|- ( ( W e. X /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x 
 |-  X = ( ( N + 1 ) WWalksN G )
2 wwlknbp1 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) )
3 simpl2 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> W e. Word ( Vtx ` G ) )
4 peano2nn0 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
5 4 3ad2ant1 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( N + 1 ) + 1 ) e. NN0 )
6 eleq1 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( # ` W ) e. NN0 <-> ( ( N + 1 ) + 1 ) e. NN0 ) )
7 6 3ad2ant3 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( # ` W ) e. NN0 <-> ( ( N + 1 ) + 1 ) e. NN0 ) )
8 5 7 mpbird 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( # ` W ) e. NN0 )
9 8 adantr 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( # ` W ) e. NN0 )
10 simpr 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> N e. NN0 )
11 nn0re 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. RR )
12 11 lep1d 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
13 12 3ad2ant1 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
14 breq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( ( N + 1 ) <_ ( # ` W ) <-> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
15 14 3ad2ant3 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( ( N + 1 ) <_ ( # ` W ) <-> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
16 13 15 mpbird 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N + 1 ) <_ ( # ` W ) )
17 16 adantr 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) <_ ( # ` W ) )
18 nn0p1elfzo 
 |-  ( ( N e. NN0 /\ ( # ` W ) e. NN0 /\ ( N + 1 ) <_ ( # ` W ) ) -> N e. ( 0 ..^ ( # ` W ) ) )
19 10 9 17 18 syl3anc 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> N e. ( 0 ..^ ( # ` W ) ) )
20 fz0add1fz1 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) )
21 9 19 20 syl2anc 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 1 ... ( # ` W ) ) )
22 3 21 jca 
 |-  ( ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
23 22 ex 
 |-  ( ( ( N + 1 ) e. NN0 /\ W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
24 2 23 syl 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
25 24 1 eleq2s 
 |-  ( W e. X -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) ) )
26 25 imp 
 |-  ( ( W e. X /\ N e. NN0 ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) )
27 pfxfv0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 1 ... ( # ` W ) ) ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
28 26 27 syl 
 |-  ( ( W e. X /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )