Theorem numclwwlkovf2ex 24910

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 concat <" X "> ) concat <" 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 996	. . . . . . 7 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> V USGrph E )
2		uzuzle23 11134	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
3		uznn0sub 11125	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
4	2, 3	syl 16	. . . . . . . 8 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN0 )
5	4	3ad2ant3 1019	. . . . . . 7 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) e. NN0 )
6		simp2 997	. . . . . . 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 24907	. . . . . . 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 1228	. . . . . 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 12604	. . . . . . . . . . . . . . . . 17 |- ( ( P e. Word V /\ X e. V ) -> ( P concat <" X "> ) e. Word V )
12	11	ex 434	. . . . . . . . . . . . . . . 16 |- ( P e. Word V -> ( X e. V -> ( P concat <" X "> ) e. Word V ) )
13	12	3ad2ant1 1017	. . . . . . . . . . . . . . 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 concat <" X "> ) e. Word V ) )
14	13	3ad2ant1 1017	. . . . . . . . . . . . . 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 concat <" X "> ) e. Word V ) )
15	14	com12 31	. . . . . . . . . . . . 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 concat <" X "> ) e. Word V ) )
16	15	3ad2ant2 1018	. . . . . . . . . . . 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 concat <" X "> ) e. Word V ) )
17	16	imp 429	. . . . . . . . . . 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 concat <" X "> ) e. Word V )
18	17	adantr 465	. . . . . . . . . 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 concat <" X "> ) e. Word V )
19		nbgraisvtx 24254	. . . . . . . . . . . . . 14 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
20		s1cl 12594	. . . . . . . . . . . . . 14 |- ( Q e. V -> <" Q "> e. Word V )
21	19, 20	syl6 33	. . . . . . . . . . . . 13 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> <" Q "> e. Word V ) )
22	21	3ad2ant1 1017	. . . . . . . . . . . 12 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> <" Q "> e. Word V ) )
23	22	adantr 465	. . . . . . . . . . 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 429	. . . . . . . . . 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 12573	. . . . . . . . . 10 |- ( ( ( P concat <" X "> ) e. Word V /\ <" Q "> e. Word V ) -> ( ( P concat <" X "> ) concat <" Q "> ) e. Word V )
26	18, 24, 25	syl2anc 661	. . . . . . . . 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 concat <" X "> ) concat <" Q "> ) e. Word V )
27		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> P e. Word V )
28	27	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . . 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 11847	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i e. NN0 )
31	30	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( P e. Word V -> ( # ` P ) e. NN0 )
33		elfzo0 11843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) <-> ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) )
34		nn0re 10816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( i e. NN0 -> i e. RR )
35	34	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> i e. RR )
36		nn0re 10816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
37		peano2rem 9898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( # ` P ) e. RR -> ( ( # ` P ) - 1 ) e. RR )
38	36, 37	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. RR )
39	38	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 1 ) e. RR )
40	36	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( # ` P ) e. RR )
41	35, 39, 40	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) )
42	36	ltm1d 10490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) < ( # ` P ) )
43	42	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( # ` P ) - 1 ) < ( # ` P ) )
44		lttr 9673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) -> ( ( i < ( ( # ` P ) - 1 ) /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) -> i < ( # ` P ) ) )
45	44	expcomd 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. RR /\ ( ( # ` P ) - 1 ) e. RR /\ ( # ` P ) e. RR ) -> ( ( ( # ` P ) - 1 ) < ( # ` P ) -> ( i < ( ( # ` P ) - 1 ) -> i < ( # ` P ) ) ) )
46	41, 43, 45	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i < ( ( # ` P ) - 1 ) -> i < ( # ` P ) ) )
47	46	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( i e. NN0 /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
48	47	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
49	33, 48	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> i < ( # ` P ) ) )
50	32, 49	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( P e. Word V -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> i < ( # ` P ) ) )
51	50	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . . . . . . 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 1176	. . . . . . . . . . . . . . . . . . . . . . . . 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 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
57	56	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( Q e. ( <. V , E >. Neighbors X ) -> ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> Q e. V ) )
58	57	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 532	. . . . . . . . . . . . . . . . . . . . . . . . . 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 465	. . . . . . . . . . . . . . . . . . . . . . . . 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 12622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( P e. Word V /\ i e. NN0 /\ i < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) = ( P ` i ) )
63	62	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ i e. NN0 /\ i < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( P ` i ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) )
64	54, 61, 63	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) )
65		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> P e. Word V )
66		peano2nn0 10848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( i e. NN0 -> ( i + 1 ) e. NN0 )
67	66	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( i + 1 ) e. NN0 )
68	33, 67	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( i + 1 ) e. NN0 )
69	68	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( i + 1 ) e. NN0 )
70		1re 9607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- 1 e. RR
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> 1 e. RR )
72	35, 71, 40	ltaddsubd 10164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( ( i + 1 ) < ( # ` P ) <-> i < ( ( # ` P ) - 1 ) ) )
73	72	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( i e. NN0 /\ ( # ` P ) e. NN0 ) -> ( i < ( ( # ` P ) - 1 ) -> ( i + 1 ) < ( # ` P ) ) )
74	73	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( i e. NN0 /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
75	74	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ i < ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
76	33, 75	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( ( # ` P ) e. NN0 -> ( i + 1 ) < ( # ` P ) ) )
77	32, 76	mpan9 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( i + 1 ) < ( # ` P ) )
78	65, 69, 77	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( P e. Word V /\ i e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) )
79	78	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( P e. Word V -> ( i e. ( 0..^ ( ( # ` P ) - 1 ) ) -> ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) ) )
80	79	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
81	80	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
82	81	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
83		ccat2s1fvw 12622	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( P e. Word V /\ ( i + 1 ) e. NN0 /\ ( i + 1 ) < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
84	82, 61, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) = ( P ` ( i + 1 ) ) )
85	84	eqcomd 2475	. . . . . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) )
86	64, 85	preq12d 4120	. . . . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } )
87	86	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
88	87	ralbidva 2903	. . . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
89	88	biimpd 207	. . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
90	89	exp41 610	. . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) )
91	90	com15 93	. . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) )
92	91	expd 436	. . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) ) )
93	92	com12 31	. . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) ) ) )
94	93	3imp 1190	. . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) ) )
95	94	3impib 1194	. . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) ) )
96	95	impcom 430	. . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
97	96	imp 429	. . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E )
98		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> P e. Word V )
99		oveq1 6302	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( # ` P ) = ( N - 2 ) -> ( ( # ` P ) - 1 ) = ( ( N - 2 ) - 1 ) )
100	99	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) = ( ( N - 2 ) - 1 ) )
101		eluzelcn 11105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> N e. CC )
102		2cnd 10620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
103		ax-1cn 9562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- 1 e. CC
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
105	101, 102, 104	subsub4d 9973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) = ( N - ( 2 + 1 ) ) )
106		2p1e3 10671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 2 + 1 ) = 3
107	106	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) = 3 )
108	107	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) = ( N - 3 ) )
109		uznn0sub 11125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. ( ZZ>= ` 3 ) -> ( N - 3 ) e. NN0 )
110	108, 109	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 + 1 ) ) e. NN0 )
111	105, 110	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) e. NN0 )
112	111	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( N - 2 ) - 1 ) e. NN0 )
113	100, 112	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( # ` P ) = ( N - 2 ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) e. NN0 )
114	113	adantll 713	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) e. NN0 )
115	32, 42	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( P e. Word V -> ( ( # ` P ) - 1 ) < ( # ` P ) )
116	115	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( ( # ` P ) - 1 ) < ( # ` P ) )
117	98, 114, 116	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P e. Word V /\ ( # ` P ) = ( N - 2 ) ) /\ N e. ( ZZ>= ` 3 ) ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) )
118	117	exp31 604	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( P e. Word V -> ( ( # ` P ) = ( N - 2 ) -> ( N e. ( ZZ>= ` 3 ) -> ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) ) ) )
119	118	a1dd 46	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
120	119	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
121	120	3imp 1190	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
122	121	com12 31	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
123	122	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 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 ) ) ) )
124	123	imp 429	. . . . . . . . . . . . . . . . 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 ) ) )
125	124	adantr 465	. . . . . . . . . . . . . . . 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 ) ) )
126	19	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
127		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( V USGrph E /\ X e. V ) -> X e. V )
128	127	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> X e. V )
129	126, 128	jctild 543	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( P e. Word V /\ ( V USGrph E /\ X e. V ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) )
130	129	ex 434	. . . . . . . . . . . . . . . . . . . . 21 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V /\ Q e. V ) ) ) )
131	130	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 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 ) ) ) )
132	131	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
133	132	com12 31	. . . . . . . . . . . . . . . . . 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 ) ) ) )
134	133	3adant3 1016	. . . . . . . . . . . . . . . . 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 ) ) ) )
135	134	imp31 432	. . . . . . . . . . . . . . . 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 ) )
136		ccat2s1fvw 12622	. . . . . . . . . . . . . . . 16 |- ( ( ( P e. Word V /\ ( ( # ` P ) - 1 ) e. NN0 /\ ( ( # ` P ) - 1 ) < ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
137	125, 135, 136	syl2anc 661	. . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) = ( P ` ( ( # ` P ) - 1 ) ) )
138		nn0cn 10817	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` P ) e. NN0 -> ( # ` P ) e. CC )
139		npcan 9841	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( # ` P ) e. CC /\ 1 e. CC ) -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
140	138, 103, 139	sylancl 662	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( # ` P ) e. NN0 -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
141	32, 140	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( P e. Word V -> ( ( ( # ` P ) - 1 ) + 1 ) = ( # ` P ) )
142	141	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 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 ) )
143	142	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 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 ) )
144	143	ad2antlr 726	. . . . . . . . . . . . . . . . 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 ) )
145	144	fveq2d 5876	. . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) )
146		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> P e. Word V )
147		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( # ` P ) = ( # ` P ) )
148	146, 147	jca 532	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) )
149	148	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) )
150	127	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> X e. V )
151	19	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> Q e. V ) )
152	151	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> Q e. V )
153		ccatw2s1p1 12620	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X )
154	149, 150, 152, 153	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) /\ Q e. ( <. V , E >. Neighbors X ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X )
155	154	ex 434	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( V USGrph E /\ X e. V ) /\ P e. Word V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) )
156	155	expcom 435	. . . . . . . . . . . . . . . . . . . . 21 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) ) )
157	156	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) ) )
158	157	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) ) )
159	158	com12 31	. . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) ) )
160	159	3adant3 1016	. . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X ) ) )
161	160	imp31 432	. . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X )
162	145, 161	eqtrd 2508	. . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) = X )
163	137, 162	preq12d 4120	. . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } = { ( P ` ( ( # ` P ) - 1 ) ) , X } )
164		lsw 12565	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. Word V -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
165	164	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( lastS ` P ) = ( P ` ( ( # ` P ) - 1 ) ) )
166		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( P ` 0 ) = X )
167	165, 166	preq12d 4120	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> { ( lastS ` P ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 1 ) ) , X } )
168	167	eleq1d 2536	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E <-> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
169	168	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( P ` 0 ) = X /\ P e. Word V ) -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
170	169	ex 434	. . . . . . . . . . . . . . . . . . . 20 |- ( ( P ` 0 ) = X -> ( P e. Word V -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) ) )
171	170	com3l 81	. . . . . . . . . . . . . . . . . . 19 |- ( P e. Word V -> ( { ( lastS ` P ) , ( P ` 0 ) } e. ran E -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) ) )
172	171	imp 429	. . . . . . . . . . . . . . . . . 18 |- ( ( P e. Word V /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) -> ( ( P ` 0 ) = X -> { ( P ` ( ( # ` P ) - 1 ) ) , X } e. ran E ) )
173	172	3adant2 1015	. . . . . . . . . . . . . . . . 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 ) )
174	173	a1d 25	. . . . . . . . . . . . . . . 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 ) ) )
175	174	3imp 1190	. . . . . . . . . . . . . . 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 )
176	175	ad2antlr 726	. . . . . . . . . . . . . 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 )
177	163, 176	eqeltrd 2555	. . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E )
178		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( # ` P ) = ( # ` P )
179	178, 153	mpanl2 681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) = X )
180		ccatw2s1p2 12621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( P e. Word V /\ ( # ` P ) = ( # ` P ) ) /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) = Q )
181	178, 180	mpanl2 681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) = Q )
182	179, 181	preq12d 4120	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( P e. Word V /\ ( X e. V /\ Q e. V ) ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } )
183	182	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. V /\ Q e. V ) -> ( P e. Word V -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) )
184	183	expcom 435	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Q e. V -> ( X e. V -> ( P e. Word V -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
185	19, 184	syl6 33	. . . . . . . . . . . . . . . . . . . . . 22 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> ( X e. V -> ( P e. Word V -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
186	185	com24 87	. . . . . . . . . . . . . . . . . . . . 21 |- ( V USGrph E -> ( P e. Word V -> ( X e. V -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
187	186	com12 31	. . . . . . . . . . . . . . . . . . . 20 |- ( P e. Word V -> ( V USGrph E -> ( X e. V -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) ) )
188	187	impd 431	. . . . . . . . . . . . . . . . . . 19 |- ( P e. Word V -> ( ( V USGrph E /\ X e. V ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
189	188	3ad2ant1 1017	. . . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
190	189	3ad2ant1 1017	. . . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
191	190	com12 31	. . . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
192	191	3adant3 1016	. . . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } ) ) )
193	192	imp31 432	. . . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } = { X , Q } )
194		nbgraeledg 24253	. . . . . . . . . . . . . . . . . 18 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) <-> { Q , X } e. ran E ) )
195		prcom 4111	. . . . . . . . . . . . . . . . . . . 20 |- { Q , X } = { X , Q }
196	195	eleq1i 2544	. . . . . . . . . . . . . . . . . . 19 |- ( { Q , X } e. ran E <-> { X , Q } e. ran E )
197	196	biimpi 194	. . . . . . . . . . . . . . . . . 18 |- ( { Q , X } e. ran E -> { X , Q } e. ran E )
198	194, 197	syl6bi 228	. . . . . . . . . . . . . . . . 17 |- ( V USGrph E -> ( Q e. ( <. V , E >. Neighbors X ) -> { X , Q } e. ran E ) )
199	198	3ad2ant1 1017	. . . . . . . . . . . . . . . 16 |- ( ( V USGrph E /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( Q e. ( <. V , E >. Neighbors X ) -> { X , Q } e. ran E ) )
200	199	adantr 465	. . . . . . . . . . . . . . 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 ) )
201	200	imp 429	. . . . . . . . . . . . . 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 )
202	193, 201	eqeltrd 2555	. . . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E )
203		ovex 6320	. . . . . . . . . . . . . 14 |- ( ( # ` P ) - 1 ) e. _V
204		fvex 5882	. . . . . . . . . . . . . 14 |- ( # ` P ) e. _V
205		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = ( ( # ` P ) - 1 ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) )
206		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( i = ( ( # ` P ) - 1 ) -> ( i + 1 ) = ( ( ( # ` P ) - 1 ) + 1 ) )
207	206	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( i = ( ( # ` P ) - 1 ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) )
208	205, 207	preq12d 4120	. . . . . . . . . . . . . . 15 |- ( i = ( ( # ` P ) - 1 ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } = { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } )
209	208	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( i = ( ( # ` P ) - 1 ) -> ( { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E ) )
210		fveq2 5872	. . . . . . . . . . . . . . . 16 |- ( i = ( # ` P ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) )
211		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( i = ( # ` P ) -> ( i + 1 ) = ( ( # ` P ) + 1 ) )
212	211	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( i = ( # ` P ) -> ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) = ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) )
213	210, 212	preq12d 4120	. . . . . . . . . . . . . . 15 |- ( i = ( # ` P ) -> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } = { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } )
214	213	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( i = ( # ` P ) -> ( { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E ) )
215	203, 204, 209, 214	ralpr 4086	. . . . . . . . . . . . 13 |- ( A. i e. { ( ( # ` P ) - 1 ) , ( # ` P ) } { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E <-> ( { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) - 1 ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( ( # ` P ) - 1 ) + 1 ) ) } e. ran E /\ { ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( # ` P ) ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( ( # ` P ) + 1 ) ) } e. ran E ) )
216	177, 202, 215	sylanbrc 664	. . . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E )
217	97, 216	jca 532	. . . . . . . . . . 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 concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E /\ A. i e. { ( ( # ` P ) - 1 ) , ( # ` P ) } { ( ( ( P concat <" X "> ) concat <" Q "> ) ` i ) , ( ( ( P concat <" X "> ) concat <" Q "> ) ` ( i + 1 ) ) } e. ran E ) )
218		2cnd 10620	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( # ` P ) e. NN0 -> 2 e. CC )
219	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( # ` P ) e. NN0 -> 1 e. CC )
220	138, 218, 219	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( # ` P ) e. NN0 -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
221	32, 220	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( P e. Word V -> ( ( # ` P ) e. CC /\ 2 e. CC /\ 1 e. CC ) )
222	221	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . . 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 ) )
223	222	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
224		addsubass 9842	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( # ` P ) e. CC /\ 2 e.