Metamath Proof Explorer

Theorem wwlksnextproplem3

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

Ref Expression
Hypotheses wwlksnextprop.x 
|- X = ( ( N + 1 ) WWalksN G )
wwlksnextprop.e 
|- E = ( Edg ` G )
wwlksnextprop.y 
|- Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
Assertion wwlksnextproplem3 
|- ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. Y )

Proof

Step Hyp Ref Expression
1 wwlksnextprop.x 
 |-  X = ( ( N + 1 ) WWalksN G )
2 wwlksnextprop.e 
 |-  E = ( Edg ` G )
3 wwlksnextprop.y 
 |-  Y = { w e. ( N WWalksN G ) | ( w ` 0 ) = P }
4 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
5 iswwlksn 
 |-  ( ( N + 1 ) e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) )
6 4 5 syl 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) <-> ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) ) )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 wwlkbp 
 |-  ( W e. ( WWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) ) )
9 lencl 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) e. NN0 )
10 eqcom 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) <-> ( ( N + 1 ) + 1 ) = ( # ` W ) )
11 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
12 11 adantr 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> ( # ` W ) e. CC )
13 1cnd 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> 1 e. CC )
14 nn0cn 
 |-  ( ( N + 1 ) e. NN0 -> ( N + 1 ) e. CC )
15 4 14 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
16 15 adantl 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> ( N + 1 ) e. CC )
17 subadd2 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC /\ ( N + 1 ) e. CC ) -> ( ( ( # ` W ) - 1 ) = ( N + 1 ) <-> ( ( N + 1 ) + 1 ) = ( # ` W ) ) )
18 17 bicomd 
 |-  ( ( ( # ` W ) e. CC /\ 1 e. CC /\ ( N + 1 ) e. CC ) -> ( ( ( N + 1 ) + 1 ) = ( # ` W ) <-> ( ( # ` W ) - 1 ) = ( N + 1 ) ) )
19 12 13 16 18 syl3anc 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> ( ( ( N + 1 ) + 1 ) = ( # ` W ) <-> ( ( # ` W ) - 1 ) = ( N + 1 ) ) )
20 10 19 syl5bb 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) <-> ( ( # ` W ) - 1 ) = ( N + 1 ) ) )
21 eqcom 
 |-  ( ( ( # ` W ) - 1 ) = ( N + 1 ) <-> ( N + 1 ) = ( ( # ` W ) - 1 ) )
22 21 biimpi 
 |-  ( ( ( # ` W ) - 1 ) = ( N + 1 ) -> ( N + 1 ) = ( ( # ` W ) - 1 ) )
23 20 22 syl6bi 
 |-  ( ( ( # ` W ) e. NN0 /\ N e. NN0 ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N + 1 ) = ( ( # ` W ) - 1 ) ) )
24 23 ex 
 |-  ( ( # ` W ) e. NN0 -> ( N e. NN0 -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N + 1 ) = ( ( # ` W ) - 1 ) ) ) )
25 24 com23 
 |-  ( ( # ` W ) e. NN0 -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) = ( ( # ` W ) - 1 ) ) ) )
26 9 25 syl 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) = ( ( # ` W ) - 1 ) ) ) )
27 8 26 simpl2im 
 |-  ( W e. ( WWalks ` G ) -> ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( N e. NN0 -> ( N + 1 ) = ( ( # ` W ) - 1 ) ) ) )
28 27 imp31 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) = ( ( # ` W ) - 1 ) )
29 28 oveq2d 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) = ( W prefix ( ( # ` W ) - 1 ) ) )
30 simpll 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> W e. ( WWalks ` G ) )
31 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
32 2re 
 |-  2 e. RR
33 32 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
34 nn0re 
 |-  ( N e. NN0 -> N e. RR )
35 33 34 addge02d 
 |-  ( N e. NN0 -> ( 0 <_ N <-> 2 <_ ( N + 2 ) ) )
36 31 35 mpbid 
 |-  ( N e. NN0 -> 2 <_ ( N + 2 ) )
37 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
38 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
39 37 38 38 addassd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
40 1p1e2 
 |-  ( 1 + 1 ) = 2
41 40 a1i 
 |-  ( N e. NN0 -> ( 1 + 1 ) = 2 )
42 41 oveq2d 
 |-  ( N e. NN0 -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
43 39 42 eqtrd 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
44 36 43 breqtrrd 
 |-  ( N e. NN0 -> 2 <_ ( ( N + 1 ) + 1 ) )
45 44 adantl 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> 2 <_ ( ( N + 1 ) + 1 ) )
46 breq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 2 <_ ( # ` W ) <-> 2 <_ ( ( N + 1 ) + 1 ) ) )
47 46 ad2antlr 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( 2 <_ ( # ` W ) <-> 2 <_ ( ( N + 1 ) + 1 ) ) )
48 45 47 mpbird 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> 2 <_ ( # ` W ) )
49 wwlksm1edg 
 |-  ( ( W e. ( WWalks ` G ) /\ 2 <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) )
50 30 48 49 syl2anc 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. ( WWalks ` G ) )
51 29 50 eqeltrd 
 |-  ( ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) )
52 51 expcom 
 |-  ( N e. NN0 -> ( ( W e. ( WWalks ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) ) )
53 6 52 sylbid 
 |-  ( N e. NN0 -> ( W e. ( ( N + 1 ) WWalksN G ) -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) ) )
54 53 com12 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) ) )
55 54 adantr 
 |-  ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) ) )
56 55 imp 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) )
57 7 2 wwlknp 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) )
58 simpll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> W e. Word ( Vtx ` G ) )
59 peano2nn0 
 |-  ( ( N + 1 ) e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
60 4 59 syl 
 |-  ( N e. NN0 -> ( ( N + 1 ) + 1 ) e. NN0 )
61 peano2re 
 |-  ( N e. RR -> ( N + 1 ) e. RR )
62 34 61 syl 
 |-  ( N e. NN0 -> ( N + 1 ) e. RR )
63 62 lep1d 
 |-  ( N e. NN0 -> ( N + 1 ) <_ ( ( N + 1 ) + 1 ) )
64 elfz2nn0 
 |-  ( ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) <-> ( ( N + 1 ) e. NN0 /\ ( ( N + 1 ) + 1 ) e. NN0 /\ ( N + 1 ) <_ ( ( N + 1 ) + 1 ) ) )
65 4 60 63 64 syl3anbrc 
 |-  ( N e. NN0 -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
66 65 adantl 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 0 ... ( ( N + 1 ) + 1 ) ) )
67 oveq2 
 |-  ( ( # ` W ) = ( ( N + 1 ) + 1 ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( ( N + 1 ) + 1 ) ) )
68 67 adantr 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( 0 ... ( # ` W ) ) = ( 0 ... ( ( N + 1 ) + 1 ) ) )
69 66 68 eleqtrrd 
 |-  ( ( ( # ` W ) = ( ( N + 1 ) + 1 ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 0 ... ( # ` W ) ) )
70 69 adantll 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( N + 1 ) e. ( 0 ... ( # ` W ) ) )
71 58 70 jca 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) /\ N e. NN0 ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) )
72 71 ex 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) )
73 72 3adant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( # ` W ) = ( ( N + 1 ) + 1 ) /\ A. i e. ( 0 ..^ ( N + 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) )
74 57 73 syl 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) )
75 74 adantr 
 |-  ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) -> ( N e. NN0 -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) ) )
76 75 imp 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) )
77 pfxlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ ( N + 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) )
78 76 77 syl 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) )
79 56 78 jca 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) /\ ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) ) )
80 iswwlksn 
 |-  ( N e. NN0 -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) /\ ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) ) ) )
81 80 adantl 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) <-> ( ( W prefix ( N + 1 ) ) e. ( WWalks ` G ) /\ ( # ` ( W prefix ( N + 1 ) ) ) = ( N + 1 ) ) ) )
82 79 81 mpbird 
 |-  ( ( ( W e. ( ( N + 1 ) WWalksN G ) /\ ( W ` 0 ) = P ) /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) )
83 82 exp31 
 |-  ( W e. ( ( N + 1 ) WWalksN G ) -> ( ( W ` 0 ) = P -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) ) )
84 83 1 eleq2s 
 |-  ( W e. X -> ( ( W ` 0 ) = P -> ( N e. NN0 -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) ) ) )
85 84 3imp 
 |-  ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) )
86 1 wwlksnextproplem1 
 |-  ( ( W e. X /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
87 86 3adant2 
 |-  ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = ( W ` 0 ) )
88 simp2 
 |-  ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( W ` 0 ) = P )
89 87 88 eqtrd 
 |-  ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( ( W prefix ( N + 1 ) ) ` 0 ) = P )
90 fveq1 
 |-  ( w = ( W prefix ( N + 1 ) ) -> ( w ` 0 ) = ( ( W prefix ( N + 1 ) ) ` 0 ) )
91 90 eqeq1d 
 |-  ( w = ( W prefix ( N + 1 ) ) -> ( ( w ` 0 ) = P <-> ( ( W prefix ( N + 1 ) ) ` 0 ) = P ) )
92 91 3 elrab2 
 |-  ( ( W prefix ( N + 1 ) ) e. Y <-> ( ( W prefix ( N + 1 ) ) e. ( N WWalksN G ) /\ ( ( W prefix ( N + 1 ) ) ` 0 ) = P ) )
93 85 89 92 sylanbrc 
 |-  ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( W prefix ( N + 1 ) ) e. Y )