This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlksnext

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

Ref Expression
Hypotheses wwlksnext.v 
|- V = ( Vtx ` G )
wwlksnext.e 
|- E = ( Edg ` G )
Assertion wwlksnext 
|- ( ( T e. ( N WWalksN G ) /\ S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) )

Proof

Step Hyp Ref Expression
1 wwlksnext.v 
 |-  V = ( Vtx ` G )
2 wwlksnext.e 
 |-  E = ( Edg ` G )
3 1 wwlknbp 
 |-  ( T e. ( N WWalksN G ) -> ( G e. _V /\ N e. NN0 /\ T e. Word V ) )
4 1 2 wwlknp 
 |-  ( T e. ( N WWalksN G ) -> ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) )
5 simp1 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) -> T e. Word V )
6 simprl 
 |-  ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> S e. V )
7 cats1un 
 |-  ( ( T e. Word V /\ S e. V ) -> ( T ++ <" S "> ) = ( T u. { <. ( # ` T ) , S >. } ) )
8 5 6 7 syl2an 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( T ++ <" S "> ) = ( T u. { <. ( # ` T ) , S >. } ) )
9 opex 
 |-  <. ( # ` T ) , S >. e. _V
10 9 snnz 
 |-  { <. ( # ` T ) , S >. } =/= (/)
11 10 neii 
 |-  -. { <. ( # ` T ) , S >. } = (/)
12 11 intnan 
 |-  -. ( T = (/) /\ { <. ( # ` T ) , S >. } = (/) )
13 df-ne 
 |-  ( ( T u. { <. ( # ` T ) , S >. } ) =/= (/) <-> -. ( T u. { <. ( # ` T ) , S >. } ) = (/) )
14 un00 
 |-  ( ( T = (/) /\ { <. ( # ` T ) , S >. } = (/) ) <-> ( T u. { <. ( # ` T ) , S >. } ) = (/) )
15 13 14 xchbinxr 
 |-  ( ( T u. { <. ( # ` T ) , S >. } ) =/= (/) <-> -. ( T = (/) /\ { <. ( # ` T ) , S >. } = (/) ) )
16 12 15 mpbir 
 |-  ( T u. { <. ( # ` T ) , S >. } ) =/= (/)
17 16 a1i 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( T u. { <. ( # ` T ) , S >. } ) =/= (/) )
18 8 17 eqnetrd 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( T ++ <" S "> ) =/= (/) )
19 s1cl 
 |-  ( S e. V -> <" S "> e. Word V )
20 19 ad2antrl 
 |-  ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> <" S "> e. Word V )
21 ccatcl 
 |-  ( ( T e. Word V /\ <" S "> e. Word V ) -> ( T ++ <" S "> ) e. Word V )
22 5 20 21 syl2an 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( T ++ <" S "> ) e. Word V )
23 simplrl 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> T e. Word V )
24 fzossfzop1 
 |-  ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
25 24 ad2antrr 
 |-  ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
26 25 sselda 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( N + 1 ) ) )
27 oveq2 
 |-  ( ( # ` T ) = ( N + 1 ) -> ( 0 ..^ ( # ` T ) ) = ( 0 ..^ ( N + 1 ) ) )
28 27 eleq2d 
 |-  ( ( # ` T ) = ( N + 1 ) -> ( i e. ( 0 ..^ ( # ` T ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
29 28 adantl 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ ( # ` T ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
30 29 ad2antlr 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( i e. ( 0 ..^ ( # ` T ) ) <-> i e. ( 0 ..^ ( N + 1 ) ) ) )
31 26 30 mpbird 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> i e. ( 0 ..^ ( # ` T ) ) )
32 ccats1val1 
 |-  ( ( T e. Word V /\ i e. ( 0 ..^ ( # ` T ) ) ) -> ( ( T ++ <" S "> ) ` i ) = ( T ` i ) )
33 23 31 32 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( T ++ <" S "> ) ` i ) = ( T ` i ) )
34 fzonn0p1p1 
 |-  ( i e. ( 0 ..^ N ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
35 34 adantl 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( N + 1 ) ) )
36 27 adantl 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( 0 ..^ ( # ` T ) ) = ( 0 ..^ ( N + 1 ) ) )
37 36 ad2antlr 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( 0 ..^ ( # ` T ) ) = ( 0 ..^ ( N + 1 ) ) )
38 35 37 eleqtrrd 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( i + 1 ) e. ( 0 ..^ ( # ` T ) ) )
39 ccats1val1 
 |-  ( ( T e. Word V /\ ( i + 1 ) e. ( 0 ..^ ( # ` T ) ) ) -> ( ( T ++ <" S "> ) ` ( i + 1 ) ) = ( T ` ( i + 1 ) ) )
40 23 38 39 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( T ++ <" S "> ) ` ( i + 1 ) ) = ( T ` ( i + 1 ) ) )
41 33 40 preq12d 
 |-  ( ( ( ( N e. NN0 /\ S e. V ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( T ` i ) , ( T ` ( i + 1 ) ) } )
42 41 exp31 
 |-  ( ( N e. NN0 /\ S e. V ) -> ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( T ` i ) , ( T ` ( i + 1 ) ) } ) ) )
43 42 adantrr 
 |-  ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( T ` i ) , ( T ` ( i + 1 ) ) } ) ) )
44 43 impcom 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( i e. ( 0 ..^ N ) -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( T ` i ) , ( T ` ( i + 1 ) ) } ) )
45 44 imp 
 |-  ( ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) /\ i e. ( 0 ..^ N ) ) -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( T ` i ) , ( T ` ( i + 1 ) ) } )
46 45 eleq1d 
 |-  ( ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) /\ i e. ( 0 ..^ N ) ) -> ( { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) )
47 46 ralbidva 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) )
48 47 exbiri 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> ( A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E -> A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) ) )
49 48 com23 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E -> ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) ) )
50 49 3impia 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) -> ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) )
51 50 imp 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E )
52 oveq1 
 |-  ( ( # ` T ) = ( N + 1 ) -> ( ( # ` T ) - 1 ) = ( ( N + 1 ) - 1 ) )
53 52 adantl 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> ( ( # ` T ) - 1 ) = ( ( N + 1 ) - 1 ) )
54 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
55 1cnd 
 |-  ( N e. NN0 -> 1 e. CC )
56 54 55 pncand 
 |-  ( N e. NN0 -> ( ( N + 1 ) - 1 ) = N )
57 56 adantl 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( ( N + 1 ) - 1 ) = N )
58 53 57 sylan9eqr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( ( # ` T ) - 1 ) = N )
59 58 fveq2d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( T ` ( ( # ` T ) - 1 ) ) = ( T ` N ) )
60 lsw 
 |-  ( T e. Word V -> ( lastS ` T ) = ( T ` ( ( # ` T ) - 1 ) ) )
61 60 ad2antrl 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( lastS ` T ) = ( T ` ( ( # ` T ) - 1 ) ) )
62 simprl 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> T e. Word V )
63 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
64 63 ad2antlr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> N e. ( 0 ..^ ( N + 1 ) ) )
65 27 eleq2d 
 |-  ( ( # ` T ) = ( N + 1 ) -> ( N e. ( 0 ..^ ( # ` T ) ) <-> N e. ( 0 ..^ ( N + 1 ) ) ) )
66 65 ad2antll 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( N e. ( 0 ..^ ( # ` T ) ) <-> N e. ( 0 ..^ ( N + 1 ) ) ) )
67 64 66 mpbird 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> N e. ( 0 ..^ ( # ` T ) ) )
68 ccats1val1 
 |-  ( ( T e. Word V /\ N e. ( 0 ..^ ( # ` T ) ) ) -> ( ( T ++ <" S "> ) ` N ) = ( T ` N ) )
69 62 67 68 syl2anc 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( ( T ++ <" S "> ) ` N ) = ( T ` N ) )
70 59 61 69 3eqtr4d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( lastS ` T ) = ( ( T ++ <" S "> ) ` N ) )
71 simpll 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> S e. V )
72 simprr 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( # ` T ) = ( N + 1 ) )
73 72 eqcomd 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( N + 1 ) = ( # ` T ) )
74 ccats1val2 
 |-  ( ( T e. Word V /\ S e. V /\ ( N + 1 ) = ( # ` T ) ) -> ( ( T ++ <" S "> ) ` ( N + 1 ) ) = S )
75 74 eqcomd 
 |-  ( ( T e. Word V /\ S e. V /\ ( N + 1 ) = ( # ` T ) ) -> S = ( ( T ++ <" S "> ) ` ( N + 1 ) ) )
76 62 71 73 75 syl3anc 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> S = ( ( T ++ <" S "> ) ` ( N + 1 ) ) )
77 70 76 preq12d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> { ( lastS ` T ) , S } = { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } )
78 77 eleq1d 
 |-  ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> ( { ( lastS ` T ) , S } e. E <-> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
79 78 biimpcd 
 |-  ( { ( lastS ` T ) , S } e. E -> ( ( ( S e. V /\ N e. NN0 ) /\ ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
80 79 exp4c 
 |-  ( { ( lastS ` T ) , S } e. E -> ( S e. V -> ( N e. NN0 -> ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) ) ) )
81 80 impcom 
 |-  ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( N e. NN0 -> ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) ) )
82 81 impcom 
 |-  ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
83 82 impcom 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E )
84 83 3adantl3 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E )
85 fveq2 
 |-  ( i = N -> ( ( T ++ <" S "> ) ` i ) = ( ( T ++ <" S "> ) ` N ) )
86 fvoveq1 
 |-  ( i = N -> ( ( T ++ <" S "> ) ` ( i + 1 ) ) = ( ( T ++ <" S "> ) ` ( N + 1 ) ) )
87 85 86 preq12d 
 |-  ( i = N -> { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } = { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } )
88 87 eleq1d 
 |-  ( i = N -> ( { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
89 88 ralsng 
 |-  ( N e. NN0 -> ( A. i e. { N } { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
90 89 ad2antrl 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( A. i e. { N } { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> { ( ( T ++ <" S "> ) ` N ) , ( ( T ++ <" S "> ) ` ( N + 1 ) ) } e. E ) )
91 84 90 mpbird 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> A. i e. { N } { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E )
92 ralunb 
 |-  ( A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E <-> ( A. i e. ( 0 ..^ N ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E /\ A. i e. { N } { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) )
93 51 91 92 sylanbrc 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> A. i e. ( ( 0 ..^ N ) u. { N } ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E )
94 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
95 eluzfz2 
 |-  ( N e. ( ZZ>= ` 0 ) -> N e. ( 0 ... N ) )
96 94 95 sylbi 
 |-  ( N e. NN0 -> N e. ( 0 ... N ) )
97 fzelp1 
 |-  ( N e. ( 0 ... N ) -> N e. ( 0 ... ( N + 1 ) ) )
98 fzosplit 
 |-  ( N e. ( 0 ... ( N + 1 ) ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. ( N ..^ ( N + 1 ) ) ) )
99 96 97 98 3syl 
 |-  ( N e. NN0 -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. ( N ..^ ( N + 1 ) ) ) )
100 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
101 fzosn 
 |-  ( N e. ZZ -> ( N ..^ ( N + 1 ) ) = { N } )
102 100 101 syl 
 |-  ( N e. NN0 -> ( N ..^ ( N + 1 ) ) = { N } )
103 102 uneq2d 
 |-  ( N e. NN0 -> ( ( 0 ..^ N ) u. ( N ..^ ( N + 1 ) ) ) = ( ( 0 ..^ N ) u. { N } ) )
104 99 103 eqtrd 
 |-  ( N e. NN0 -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
105 104 ad2antrl 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( 0 ..^ ( N + 1 ) ) = ( ( 0 ..^ N ) u. { N } ) )
106 93 105 raleqtrrdv 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> A. i e. ( 0 ..^ ( N + 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E )
107 ccatlen 
 |-  ( ( T e. Word V /\ <" S "> e. Word V ) -> ( # ` ( T ++ <" S "> ) ) = ( ( # ` T ) + ( # ` <" S "> ) ) )
108 5 20 107 syl2an 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( # ` ( T ++ <" S "> ) ) = ( ( # ` T ) + ( # ` <" S "> ) ) )
109 108 oveq1d 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( # ` ( T ++ <" S "> ) ) - 1 ) = ( ( ( # ` T ) + ( # ` <" S "> ) ) - 1 ) )
110 simpl2 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( # ` T ) = ( N + 1 ) )
111 s1len 
 |-  ( # ` <" S "> ) = 1
112 111 a1i 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( # ` <" S "> ) = 1 )
113 110 112 oveq12d 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( # ` T ) + ( # ` <" S "> ) ) = ( ( N + 1 ) + 1 ) )
114 113 oveq1d 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( ( # ` T ) + ( # ` <" S "> ) ) - 1 ) = ( ( ( N + 1 ) + 1 ) - 1 ) )
115 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
116 115 nn0cnd 
 |-  ( N e. NN0 -> ( N + 1 ) e. CC )
117 116 55 pncand 
 |-  ( N e. NN0 -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
118 117 ad2antrl 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( ( N + 1 ) + 1 ) - 1 ) = ( N + 1 ) )
119 109 114 118 3eqtrd 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( # ` ( T ++ <" S "> ) ) - 1 ) = ( N + 1 ) )
120 119 oveq2d 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) = ( 0 ..^ ( N + 1 ) ) )
121 106 120 raleqtrrdv 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E )
122 18 22 121 3jca 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) )
123 108 113 eqtrd 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) )
124 122 123 jca 
 |-  ( ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) /\ ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
125 124 ex 
 |-  ( ( T e. Word V /\ ( # ` T ) = ( N + 1 ) /\ A. i e. ( 0 ..^ N ) { ( T ` i ) , ( T ` ( i + 1 ) ) } e. E ) -> ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
126 4 125 syl 
 |-  ( T e. ( N WWalksN G ) -> ( ( N e. NN0 /\ ( S e. V /\ { ( lastS ` T ) , S } e. E ) ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
127 126 expd 
 |-  ( T e. ( N WWalksN G ) -> ( N e. NN0 -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) ) )
128 127 impcom 
 |-  ( ( N e. NN0 /\ T e. ( N WWalksN G ) ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
129 128 adantll 
 |-  ( ( ( G e. _V /\ N e. NN0 ) /\ T e. ( N WWalksN G ) ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
130 iswwlksn 
 |-  ( ( N + 1 ) e. NN0 -> ( ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) <-> ( ( T ++ <" S "> ) e. ( WWalks ` G ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
131 115 130 syl 
 |-  ( N e. NN0 -> ( ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) <-> ( ( T ++ <" S "> ) e. ( WWalks ` G ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
132 131 adantl 
 |-  ( ( G e. _V /\ N e. NN0 ) -> ( ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) <-> ( ( T ++ <" S "> ) e. ( WWalks ` G ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
133 1 2 iswwlks 
 |-  ( ( T ++ <" S "> ) e. ( WWalks ` G ) <-> ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) )
134 133 anbi1i 
 |-  ( ( ( T ++ <" S "> ) e. ( WWalks ` G ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) <-> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) )
135 132 134 bitrdi 
 |-  ( ( G e. _V /\ N e. NN0 ) -> ( ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) <-> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
136 135 adantr 
 |-  ( ( ( G e. _V /\ N e. NN0 ) /\ T e. ( N WWalksN G ) ) -> ( ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) <-> ( ( ( T ++ <" S "> ) =/= (/) /\ ( T ++ <" S "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( T ++ <" S "> ) ) - 1 ) ) { ( ( T ++ <" S "> ) ` i ) , ( ( T ++ <" S "> ) ` ( i + 1 ) ) } e. E ) /\ ( # ` ( T ++ <" S "> ) ) = ( ( N + 1 ) + 1 ) ) ) )
137 129 136 sylibrd 
 |-  ( ( ( G e. _V /\ N e. NN0 ) /\ T e. ( N WWalksN G ) ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) ) )
138 137 ex 
 |-  ( ( G e. _V /\ N e. NN0 ) -> ( T e. ( N WWalksN G ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) ) ) )
139 138 3adant3 
 |-  ( ( G e. _V /\ N e. NN0 /\ T e. Word V ) -> ( T e. ( N WWalksN G ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) ) ) )
140 3 139 mpcom 
 |-  ( T e. ( N WWalksN G ) -> ( ( S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) ) )
141 140 3impib 
 |-  ( ( T e. ( N WWalksN G ) /\ S e. V /\ { ( lastS ` T ) , S } e. E ) -> ( T ++ <" S "> ) e. ( ( N + 1 ) WWalksN G ) )