Metamath Proof Explorer

Theorem clwwlknonex2

Description: Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018) (Revised by AV, 25-Feb-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Hypotheses clwwlknonex2.v 
|- V = ( Vtx ` G )
clwwlknonex2.e 
|- E = ( Edg ` G )
Assertion clwwlknonex2 
|- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlknonex2.v 
 |-  V = ( Vtx ` G )
2 clwwlknonex2.e 
 |-  E = ( Edg ` G )
3 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
4 3 nnne0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) =/= 0 )
5 4 3ad2ant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) =/= 0 )
6 1 2 clwwlknonel 
 |-  ( ( N - 2 ) =/= 0 -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
7 5 6 syl 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) )
8 simpr11 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) -> W e. Word V )
9 8 adantr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> W e. Word V )
10 simpll1 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> X e. V )
11 simpll2 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> Y e. V )
12 ccatw2s1cl 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )
13 9 10 11 12 syl3anc 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V )
14 1 2 clwwlknonex2lem2 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
15 simp11 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> W e. Word V )
16 15 ad2antlr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> W e. Word V )
17 ccatw2s1len 
 |-  ( W e. Word V -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
18 16 17 syl 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
19 18 oveq1d 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) = ( ( ( # ` W ) + 2 ) - 1 ) )
20 19 oveq2d 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) = ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) )
21 simp3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> N e. ( ZZ>= ` 3 ) )
22 simp2 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( # ` W ) = ( N - 2 ) )
23 21 22 anim12i 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) -> ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) )
24 23 adantr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) )
25 clwwlknonex2lem1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )
26 24 25 syl 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )
27 20 26 eqtrd 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )
28 27 raleqdv 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E <-> A. i e. ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E ) )
29 14 28 mpbird 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
30 ccatws1cl 
 |-  ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
31 lswccats1 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ Y e. V ) -> ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = Y )
32 30 31 stoic3 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = Y )
33 16 10 11 32 syl3anc 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = Y )
34 3 nngt0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 < ( N - 2 ) )
35 breq2 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( 0 < ( # ` W ) <-> 0 < ( N - 2 ) ) )
36 34 35 syl5ibr 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> 0 < ( # ` W ) ) )
37 36 3ad2ant2 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( N e. ( ZZ>= ` 3 ) -> 0 < ( # ` W ) ) )
38 37 com12 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> 0 < ( # ` W ) ) )
39 38 3ad2ant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> 0 < ( # ` W ) ) )
40 39 imp 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) -> 0 < ( # ` W ) )
41 40 adantr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> 0 < ( # ` W ) )
42 ccat2s1fst 
 |-  ( ( W e. Word V /\ 0 < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) )
43 16 41 42 syl2anc 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) )
44 33 43 preq12d 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } = { Y , ( W ` 0 ) } )
45 prcom 
 |-  { X , Y } = { Y , X }
46 45 eleq1i 
 |-  ( { X , Y } e. E <-> { Y , X } e. E )
47 46 biimpi 
 |-  ( { X , Y } e. E -> { Y , X } e. E )
48 47 adantl 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { Y , X } e. E )
49 preq2 
 |-  ( ( W ` 0 ) = X -> { Y , ( W ` 0 ) } = { Y , X } )
50 49 eleq1d 
 |-  ( ( W ` 0 ) = X -> ( { Y , ( W ` 0 ) } e. E <-> { Y , X } e. E ) )
51 50 3ad2ant3 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { Y , ( W ` 0 ) } e. E <-> { Y , X } e. E ) )
52 51 ad2antlr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( { Y , ( W ` 0 ) } e. E <-> { Y , X } e. E ) )
53 48 52 mpbird 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { Y , ( W ` 0 ) } e. E )
54 44 53 eqeltrd 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E )
55 13 29 54 3jca 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) )
56 17 3ad2ant1 
 |-  ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
57 56 3ad2ant1 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
58 57 ad2antlr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )
59 oveq1 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( ( # ` W ) + 2 ) = ( ( N - 2 ) + 2 ) )
60 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
61 2cn 
 |-  2 e. CC
62 npcan 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( ( N - 2 ) + 2 ) = N )
63 60 61 62 sylancl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 2 ) = N )
64 59 63 sylan9eq 
 |-  ( ( ( # ` W ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` W ) + 2 ) = N )
65 64 ex 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( # ` W ) + 2 ) = N ) )
66 65 3ad2ant2 
 |-  ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( # ` W ) + 2 ) = N ) )
67 66 com12 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( # ` W ) + 2 ) = N ) )
68 67 3ad2ant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( ( # ` W ) + 2 ) = N ) )
69 68 imp 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) -> ( ( # ` W ) + 2 ) = N )
70 69 adantr 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( # ` W ) + 2 ) = N )
71 58 70 eqtrd 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N )
72 55 71 jca 
 |-  ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) )
73 72 exp31 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W e. Word V /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { ( lastS ` W ) , ( W ` 0 ) } e. E ) /\ ( # ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) -> ( { X , Y } e. E -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) ) )
74 7 73 sylbid 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( { X , Y } e. E -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) ) )
75 74 com23 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( { X , Y } e. E -> ( W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) ) )
76 75 3imp 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) )
77 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
78 1 2 isclwwlknx 
 |-  ( N e. NN -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) <-> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) )
79 77 78 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) <-> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) )
80 79 3ad2ant3 
 |-  ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) <-> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) )
81 80 3ad2ant1 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) <-> ( ( ( ( W ++ <" X "> ) ++ <" Y "> ) e. Word V /\ A. i e. ( 0 ..^ ( ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) - 1 ) ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E /\ { ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) } e. E ) /\ ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = N ) ) )
82 76 81 mpbird 
 |-  ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )