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 14 27 raleqtrrdv 
 |-  ( ( ( ( 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 )
29 ccatws1cl 
 |-  ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
30 lswccats1 
 |-  ( ( ( W ++ <" X "> ) e. Word V /\ Y e. V ) -> ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = Y )
31 29 30 stoic3 
 |-  ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( lastS ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = Y )
32 16 10 11 31 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 )
33 3 nngt0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 < ( N - 2 ) )
34 breq2 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( 0 < ( # ` W ) <-> 0 < ( N - 2 ) ) )
35 33 34 imbitrrid 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> 0 < ( # ` W ) ) )
36 35 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 ) ) )
37 36 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 ) ) )
38 37 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 ) ) )
39 38 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 ) )
40 39 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 ) )
41 ccat2s1fst 
 |-  ( ( W e. Word V /\ 0 < ( # ` W ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` 0 ) = ( W ` 0 ) )
42 16 40 41 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 ) )
43 32 42 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 ) } )
44 prcom 
 |-  { X , Y } = { Y , X }
45 44 eleq1i 
 |-  ( { X , Y } e. E <-> { Y , X } e. E )
46 45 biimpi 
 |-  ( { X , Y } e. E -> { Y , X } e. E )
47 46 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 )
48 preq2 
 |-  ( ( W ` 0 ) = X -> { Y , ( W ` 0 ) } = { Y , X } )
49 48 eleq1d 
 |-  ( ( W ` 0 ) = X -> ( { Y , ( W ` 0 ) } e. E <-> { Y , X } e. E ) )
50 49 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 ) )
51 50 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 ) )
52 47 51 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 )
53 43 52 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 )
54 13 28 53 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 ) )
55 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 ) )
56 55 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 ) )
57 56 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 ) )
58 oveq1 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( ( # ` W ) + 2 ) = ( ( N - 2 ) + 2 ) )
59 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
60 2cn 
 |-  2 e. CC
61 npcan 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( ( N - 2 ) + 2 ) = N )
62 59 60 61 sylancl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) + 2 ) = N )
63 58 62 sylan9eq 
 |-  ( ( ( # ` W ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` W ) + 2 ) = N )
64 63 ex 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( # ` W ) + 2 ) = N ) )
65 64 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 ) )
66 65 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 ) )
67 66 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 ) )
68 67 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 )
69 68 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 )
70 57 69 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 )
71 54 70 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 ) )
72 71 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 ) ) ) )
73 7 72 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 ) ) ) )
74 73 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 ) ) ) )
75 74 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 ) )
76 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
77 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 ) ) )
78 76 77 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 ) ) )
79 78 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 ) ) )
80 79 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 ) ) )
81 75 80 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 ) )