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 )