Theorem numclwwlkovf2ex 25814

Description: Extending a closed walk starting at a fixed vertex by an additional edge (forth and back). (Contributed by AV, 22-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.)

Hypotheses

Ref	Expression
numclwwlk.c	|- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
numclwwlk.f	|- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )

Assertion

Ref	Expression
numclwwlkovf2ex	|- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ Q e. ( <. V , E >. Neighbors X ) /\ P e. ( X F ( N - 2 ) ) ) -> ( ( P ++ <" X "> ) ++ <" Q "> ) e. ( C ` N ) )

Distinct variable groups:   n, E   n, N   n, V   w, C   w, N   C, n, v, w   v, N   n, X, v, w   v, V   w, E   w, V   w, F   w, P   w, Q

Allowed substitution hints:   P( v, n)   Q( v, n)   E( v)   F( v, n)

Proof of Theorem numclwwlkovf2ex

Dummy variable i is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp1 1008	. . . . . . 7 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V USGrph E )
2		uzuzle23 11199	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
3		uznn0sub 11190	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
4	2, 3	syl 17	. . . . . . . 8 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN0 )
5	4	3ad2ant3 1031	. . . . . . 7 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. NN0 )
6		simp2 1009	. . . . . . 7 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> X e. V )
7		numclwwlk.c	. . . . . . . 8 |- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
8		numclwwlk.f	. . . . . . . 8 |- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
9	7, 8	numclwwlkovfel2 25811	. . . . . . 7 |- ( ( V USGrph E /\ ( N - 2 ) e. NN0 /\ X e. V ) -> ( P e. ( X F ( N - 2 ) ) <-> ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) )
10	1, 5, 6, 9	syl3anc 1268	. . . . . 6 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( P e. ( X F ( N - 2 ) ) <-> ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) )
11		ccatws1cl 12753	. . . . . . . . . . . . . . . . 17 |- ( ( P e. Word V /\ X e. V ) -> ( P ++ <" X "> ) e. Word V )
12	11	ex 436	. . . . . . . . . . . . . . . 16 |- ( P e. Word V -> ( X e. V -> ( P ++ <" X "> ) e. Word V ) )
13	12	3ad2ant1 1029	. . . . . . . . . . . . . . 15 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( X e. V -> ( P ++ <" X "> ) e. Word V ) )
14	13	3ad2ant1 1029	. . . . . . . . . . . . . 14 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( X e. V -> ( P ++ <" X "> ) e. Word V ) )
15	14	com12 32	. . . . . . . . . . . . 13 |- ( X e. V -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( P ++ <" X "> ) e. Word V ) )
16	15	3ad2ant2 1030	. . . . . . . . . . . 12 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( P ++ <" X "> ) e. Word V ) )
17	16	imp 431	. . . . . . . . . . 11 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( P ++ <" X "> ) e. Word V )
18	17	adantr 467	. . . . . . . . . 10 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P ++ <" X "> ) e. Word V )
19		nbgraisvtx 25159	. . . . . . . . . . . . . 14 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
20		s1cl 12741	. . . . . . . . . . . . . 14 |- ( Q e. V -> <" Q "> e. Word V )
21	19, 20	syl6 34	. . . . . . . . . . . . 13 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> <" Q "> e. Word V ) )
22	21	3ad2ant1 1029	. . . . . . . . . . . 12 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> <" Q "> e. Word V ) )
23	22	adantr 467	. . . . . . . . . . 11 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> <" Q "> e. Word V ) )
24	23	imp 431	. . . . . . . . . 10 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> <" Q "> e. Word V )
25		ccatcl 12720	. . . . . . . . . 10 |- ( ( ( P ++ <" X "> ) e. Word V /\ <" Q "> e. Word V ) -> ( ( P ++ <" X "> ) ++ <" Q "> ) e. Word V )
26	18, 24, 25	syl2anc 667	. . . . . . . . 9 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( P ++ <" X "> ) ++ <" Q "> ) e. Word V )
27		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> P e. Word V )
28	27	ad2antlr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> P e. Word V )
29	28	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> P e. Word V )
30		elfzonn0 11960	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i e. NN0 )
31	30	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> i e. NN0 )
32		lencl 12687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( P e. Word V -> ( # ` P ) e. NN0 )
33		elfzo0 11956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) <-> ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) )
34		nn0re 10878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( i e. NN0 -> i e. RR )
35	34	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> i e. RR )
36		nn0re 10878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
37		peano2rem 9941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( # ` P ) e. RR -> ( ( # ` P ) - 1 ) e. RR )
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. RR )
39	38	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 1 ) e. RR )
40	36	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( # ` P ) e. RR )
41	35, 39, 40	3jca 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) )
42	36	ltm1d 10539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) < ( # ` P ) )
43	42	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 1 ) < ( # ` P ) )
44		lttr 9710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) -> ( ( i < ( ( # ` P ) - 1 ) /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) -> i < ( # ` P ) ) )
45	44	expcomd 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) -> ( ( ( # ` P ) - 1 ) < ( # ` P ) -> ( i < ( ( # ` P ) - 1 ) -> i < ( # ` P ) ) ) )
46	41, 43, 45	sylc 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i < ( ( # ` P ) - 1 ) -> i < ( # ` P ) ) )
47	46	impancom 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( i e. NN0 /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
48	47	3adant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
49	33, 48	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
50	32, 49	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( P e. Word V -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i < ( # ` P ) ) )
51	50	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i < ( # ` P ) ) )
52	51	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i < ( # ` P ) ) )
53	52	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> i < ( # ` P ) )
54	29, 31, 53	3jca 1188	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P e. Word V /\ i e. NN0 /\ i < ( # ` P ) ) )
55	6	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
56	19	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
57	56	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( Q e. ( <. V , E >. Neighbors X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> Q e. V ) )
58	57	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> Q e. V ) )
59	58	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> Q e. V )
60	55, 59	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( X e. V /\ Q e. V ) )
61	60	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( X e. V /\ Q e. V ) )
62		ccat2s1fvw 12771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( P e. Word V /\ i e. NN0 /\ i < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) = ( P ` i ) )
63	62	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ i e. NN0 /\ i < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( P ` i ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) )
64	54, 61, 63	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P ` i ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) )
65		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> P e. Word V )
66		peano2nn0 10910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( i e. NN0 -> ( i + 1 ) e. NN0 )
67	66	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( i + 1 ) e. NN0 )
68	33, 67	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( i + 1 ) e. NN0 )
69	68	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( i + 1 ) e. NN0 )
70		1red 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> 1 e. RR )
71	35, 70, 40	ltaddsubd 10213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( i + 1 ) < ( # ` P ) <-> i < ( ( # ` P ) - 1 ) ) )
72	71	biimprd 227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i < ( ( # ` P ) - 1 ) -> ( i + 1 ) < ( # ` P ) ) )
73	72	impancom 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
74	73	3adant2 1027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
75	33, 74	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
76	32, 75	mpan9 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( i + 1 ) < ( # ` P ) )
77	65, 69, 76	3jca 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) )
78	77	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( P e. Word V -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) ) )
79	78	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) ) )
80	79	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) ) )
81	80	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) )
82		ccat2s1fvw 12771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
83	81, 61, 82	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
84	83	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P ` ( i + 1 ) ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) )
85	64, 84	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> { ( P ` i ) , ( P ` ( i + 1 ) ) } = { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } )
86	85	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
87	86	ralbidva 2824	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E <-> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
88	87	biimpd 211	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( Q e. ( <. V , E >. Neighbors X ) /\ ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) /\ ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
89	88	exp41 615	. . . . . . . . . . . . . . . . . . 19 |- ( Q e. ( <. V , E >. Neighbors X ) -> ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) )
90	89	com15 96	. . . . . . . . . . . . . . . . . 18 |- ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) )
91	90	expd 438	. . . . . . . . . . . . . . . . 17 |- ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( P e. Word V -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> ( ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) ) )
92	91	com12 32	. . . . . . . . . . . . . . . 16 |- ( P e. Word V -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> ( ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) ) )
93	92	3imp 1202	. . . . . . . . . . . . . . 15 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) )
94	93	3impib 1206	. . . . . . . . . . . . . 14 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) )
95	94	impcom 432	. . . . . . . . . . . . 13 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
96	95	imp 431	. . . . . . . . . . . 12 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E )
97		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> P e. Word V )
98		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( # ` P ) = ( N - 2 ) -> ( ( # ` P ) - 1 ) = ( ( N - 2 ) - 1 ) )
99	98	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) = ( ( N - 2 ) - 1 ) )
100		eluzelcn 11170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> N e. CC )
101		2cnd 10682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
102		1cnd 9659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
103	100, 101, 102	subsub4d 10017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) = ( N - ( 2 + 1 ) ) )
104		2p1e3 10733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 2 + 1 ) = 3
105	104	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) = 3 )
106	105	oveq2d 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) = ( N - 3 ) )
107		uznn0sub 11190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 3 ) e. NN0 )
108	106, 107	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) e. NN0 )
109	103, 108	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) e. NN0 )
110	109	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) - 1 ) e. NN0 )
111	99, 110	eqeltrd 2529	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) e. NN0 )
112	111	adantll 720	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) e. NN0 )
113	32, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. Word V -> ( ( # ` P ) - 1 ) < ( # ` P ) )
114	113	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) < ( # ` P ) )
115	97, 112, 114	3jca 1188	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) )
116	115	exp31 609	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. Word V -> ( ( # ` P ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) ) )
117	116	a1dd 47	. . . . . . . . . . . . . . . . . . . . . 22 |- ( P e. Word V -> ( ( # ` P ) = ( N - 2 ) -> ( ( P ` 0 ) = X -> ( N e. ( ZZ>= ` 3 ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) ) ) )
118	117	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( # ` P ) = ( N - 2 ) -> ( ( P ` 0 ) = X -> ( N e. ( ZZ>= ` 3 ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) ) ) )
119	118	3imp 1202	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( N e. ( ZZ>= ` 3 ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) )
120	119	com12 32	. . . . . . . . . . . . . . . . . . 19 |- ( N e. ( ZZ>= ` 3 ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) )
121	120	3ad2ant3 1031	. . . . . . . . . . . . . . . . . 18 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) )
122	121	imp 431	. . . . . . . . . . . . . . . . 17 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) )
123	122	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) )
124	19	ad2antrl 734	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
125		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( V USGrph E /\ X e. V ) -> X e. V )
126	125	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> X e. V )
127	124, 126	jctild 546	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) )
128	127	ex 436	. . . . . . . . . . . . . . . . . . . . 21 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
129	128	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . 20 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
130	129	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
131	130	com12 32	. . . . . . . . . . . . . . . . . 18 |- ( ( V USGrph E /\ X e. V ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
132	131	3adant3 1028	. . . . . . . . . . . . . . . . 17 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
133	132	imp31 434	. . . . . . . . . . . . . . . 16 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( X e. V /\ Q e. V ) )
134		ccat2s1fvw 12771	. . . . . . . . . . . . . . . 16 |- ( ( ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
135	123, 133, 134	syl2anc 667	. . . . . . . . . . . . . . 15 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
136		nn0cn 10879	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` P ) e. NN0 -> ( # ` P ) e. CC )
137		ax-1cn 9597	. . . . . . . . . . . . . . . . . . . . . 22 |- 1 e. CC
138		npcan 9884	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( # ` P ) e. CC /\ 1 e. CC ) -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
139	136, 137, 138	sylancl 668	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
140	32, 139	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( P e. Word V -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
141	140	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . 19 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
142	141	3ad2ant1 1029	. . . . . . . . . . . . . . . . . 18 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
143	142	ad2antlr 733	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
144	143	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) )
145		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> P e. Word V )
146		eqidd 2452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( # ` P ) = ( # ` P ) )
147	145, 146	jca 535	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) )
148	147	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) )
149	125	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> X e. V )
150	19	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
151	150	imp 431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> Q e. V )
152		ccatw2s1p1 12769	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X )
153	148, 149, 151, 152	syl12anc 1266	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X )
154	153	ex 436	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) )
155	154	expcom 437	. . . . . . . . . . . . . . . . . . . . 21 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) ) )
156	155	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . 20 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) ) )
157	156	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) ) )
158	157	com12 32	. . . . . . . . . . . . . . . . . 18 |- ( ( V USGrph E /\ X e. V ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) ) )
159	158	3adant3 1028	. . . . . . . . . . . . . . . . 17 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X ) ) )
160	159	imp31 434	. . . . . . . . . . . . . . . 16 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X )
161	144, 160	eqtrd 2485	. . . . . . . . . . . . . . 15 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) = X )
162	135, 161	preq12d 4059	. . . . . . . . . . . . . 14 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } = { ( P ` ( ( # ` P ) - 1 ) ) , X } )
163		lsw 12711	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
164	163	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
165		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( P ` 0 ) = X )
166	164, 165	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> { ( lastS ` P ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 1 ) ) , X } )
167	166	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
168	167	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
169	168	ex 436	. . . . . . . . . . . . . . . . . . . 20 |- ( ( P ` 0 ) = X -> ( P e. Word V -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) ) )
170	169	com3l 84	. . . . . . . . . . . . . . . . . . 19 |- ( P e. Word V -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) ) )
171	170	imp 431	. . . . . . . . . . . . . . . . . 18 |- ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
172	171	3adant2 1027	. . . . . . . . . . . . . . . . 17 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
173	172	a1d 26	. . . . . . . . . . . . . . . 16 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( # ` P ) = ( N - 2 ) -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) ) )
174	173	3imp 1202	. . . . . . . . . . . . . . 15 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E )
175	174	ad2antlr 733	. . . . . . . . . . . . . 14 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E )
176	162, 175	eqeltrd 2529	. . . . . . . . . . . . 13 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E )
177		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( # ` P ) = ( # ` P )
178	177, 152	mpanl2 687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) = X )
179		ccatw2s1p2 12770	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) = Q )
180	177, 179	mpanl2 687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) = Q )
181	178, 180	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } )
182	181	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. V /\ Q e. V ) -> ( P e. Word V -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) )
183	182	expcom 437	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Q e. V -> ( X e. V -> ( P e. Word V -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
184	19, 183	syl6 34	. . . . . . . . . . . . . . . . . . . . . 22 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V -> ( P e. Word V -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
185	184	com24 90	. . . . . . . . . . . . . . . . . . . . 21 |- ( V USGrph E -> ( P e. Word V -> ( X e. V -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
186	185	com12 32	. . . . . . . . . . . . . . . . . . . 20 |- ( P e. Word V -> ( V USGrph E -> ( X e. V -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
187	186	impd 433	. . . . . . . . . . . . . . . . . . 19 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
188	187	3ad2ant1 1029	. . . . . . . . . . . . . . . . . 18 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
189	188	3ad2ant1 1029	. . . . . . . . . . . . . . . . 17 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
190	189	com12 32	. . . . . . . . . . . . . . . 16 |- ( ( V USGrph E /\ X e. V ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
191	190	3adant3 1028	. . . . . . . . . . . . . . 15 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
192	191	imp31 434	. . . . . . . . . . . . . 14 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } )
193		nbgraeledg 25158	. . . . . . . . . . . . . . . . . 18 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) <-> { Q , X } e. ran E ) )
194		prcom 4050	. . . . . . . . . . . . . . . . . . . 20 |- { Q , X } = { X , Q }
195	194	eleq1i 2520	. . . . . . . . . . . . . . . . . . 19 |- ( { Q , X } e. ran E <-> { X , Q } e. ran E )
196	195	biimpi 198	. . . . . . . . . . . . . . . . . 18 |- ( { Q , X } e. ran E -> { X , Q } e. ran E )
197	193, 196	syl6bi 232	. . . . . . . . . . . . . . . . 17 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> { X , Q } e. ran E ) )
198	197	3ad2ant1 1029	. . . . . . . . . . . . . . . 16 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { X , Q } e. ran E ) )
199	198	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { X , Q } e. ran E ) )
200	199	imp 431	. . . . . . . . . . . . . 14 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { X , Q } e. ran E )
201	192, 200	eqeltrd 2529	. . . . . . . . . . . . 13 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E )
202		ovex 6318	. . . . . . . . . . . . . 14 |- ( ( # ` P ) - 1 ) e. _V
203		fvex 5875	. . . . . . . . . . . . . 14 |- ( # ` P ) e. _V
204		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( i = ( ( # ` P ) - 1 ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) )
205		oveq1 6297	. . . . . . . . . . . . . . . . 17 |- ( i = ( ( # ` P ) - 1 ) -> ( i + 1 ) = ( ( ( # ` P ) - 1 ) + 1 ) )
206	205	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( i = ( ( # ` P ) - 1 ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) )
207	204, 206	preq12d 4059	. . . . . . . . . . . . . . 15 |- ( i = ( ( # ` P ) - 1 ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } = { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } )
208	207	eleq1d 2513	. . . . . . . . . . . . . 14 |- ( i = ( ( # ` P ) - 1 ) -> ( { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E ) )
209		fveq2 5865	. . . . . . . . . . . . . . . 16 |- ( i = ( # ` P ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) )
210		oveq1 6297	. . . . . . . . . . . . . . . . 17 |- ( i = ( # ` P ) -> ( i + 1 ) = ( ( # ` P ) + 1 ) )
211	210	fveq2d 5869	. . . . . . . . . . . . . . . 16 |- ( i = ( # ` P ) -> ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) = ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) )
212	209, 211	preq12d 4059	. . . . . . . . . . . . . . 15 |- ( i = ( # ` P ) -> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } = { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } )
213	212	eleq1d 2513	. . . . . . . . . . . . . 14 |- ( i = ( # ` P ) -> ( { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E ) )
214	202, 203, 208, 213	ralpr 4025	. . . . . . . . . . . . 13 |- ( A. i e. { ( ( # ` P ) - 1 ) , ( # ` P ) } { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> ( { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E /\ { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( # ` P ) ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E ) )
215	176, 201, 214	sylanbrc 670	. . . . . . . . . . . 12 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> A. i e. { ( ( # ` P ) - 1 ) , ( # ` P ) } { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E )
216	96, 215	jca 535	. . . . . . . . . . 11 |- ( ( ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( # ` P ) = ( N - 2 ) /\ ( P ` 0 ) = X ) ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E /\ A. i e. { ( ( # ` P ) - 1 ) , ( # ` P ) } { ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` i ) , ( ( ( P ++ <" X "> ) ++ <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
217		2cnd 10682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( # ` P ) e. NN0 -> 2 e. CC )
218		1cnd 9659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( # ` P ) e. NN0 -> 1 e. CC )
219	136, 217, 218	3jca 1188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
220	32, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. Word V -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
221	220	3ad2ant1 1029	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
222	221	adantr 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( P e. Word V /\ A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) /\ ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
223		addsubass 9885	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( ( # ` P ) + 2 ) - 1 ) = ( ( # `