Theorem numclwlk2lem2f 24927

Description: R is a function. (Contributed by Alexander van der Vekens, 5-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 } )
numclwwlk.g	|- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
numclwwlk.q	|- Q = ( v e. V , n e. NN0 |-> { w e. ( ( V WWalksN E ) ` n ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h	|- H = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) =/= ( w ` 0 ) ) } )
numclwwlk.r	|- R = ( x e. ( X H ( N + 2 ) ) |-> ( x substr <. 0 , ( N + 1 ) >. ) )

Assertion

Ref	Expression
numclwlk2lem2f	|- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )

Distinct variable groups:   n, E   n, N   n, V   w, C, x   x, E   w, N, x   x, V   C, n, v, w   v, N   n, X, v, w   v, V   w, E   w, V   w, F   w, Q   w, G   x, X   v, E   x, H   x, Q

Allowed substitution hints:   Q( v, n)   R( x, w, v, n)   F( x, v, n)   G( x, v, n)   H( w, v, n)

Proof of Theorem numclwlk2lem2f

Step	Hyp	Ref	Expression
1		nnnn0 10814	. . . . . . . . . 10 |- ( N e. NN -> N e. NN0 )
2		2nn0 10824	. . . . . . . . . . 11 |- 2 e. NN0
3	2	a1i 11	. . . . . . . . . 10 |- ( N e. NN -> 2 e. NN0 )
4	1, 3	nn0addcld 10868	. . . . . . . . 9 |- ( N e. NN -> ( N + 2 ) e. NN0 )
5	4	anim2i 569	. . . . . . . 8 |- ( ( X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. NN0 ) )
6	5	3adant1 1014	. . . . . . 7 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. NN0 ) )
7		numclwwlk.c	. . . . . . . . 9 |- C = ( n e. NN0 |-> ( ( V ClWWalksN E ) ` n ) )
8		numclwwlk.f	. . . . . . . . 9 |- F = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( w ` 0 ) = v } )
9		numclwwlk.g	. . . . . . . . 9 |- G = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) = ( w ` 0 ) ) } )
10		numclwwlk.q	. . . . . . . . 9 |- Q = ( v e. V , n e. NN0 |-> { w e. ( ( V WWalksN E ) ` n ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
11		numclwwlk.h	. . . . . . . . 9 |- H = ( v e. V , n e. NN0 |-> { w e. ( C ` n ) | ( ( w ` 0 ) = v /\ ( w ` ( n - 2 ) ) =/= ( w ` 0 ) ) } )
12	7, 8, 9, 10, 11	numclwwlkovh 24925	. . . . . . . 8 |- ( ( X e. V /\ ( N + 2 ) e. NN0 ) -> ( X H ( N + 2 ) ) = { w e. ( C ` ( N + 2 ) ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } )
13	12	eleq2d 2537	. . . . . . 7 |- ( ( X e. V /\ ( N + 2 ) e. NN0 ) -> ( x e. ( X H ( N + 2 ) ) <-> x e. { w e. ( C ` ( N + 2 ) ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
14	6, 13	syl 16	. . . . . 6 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> x e. { w e. ( C ` ( N + 2 ) ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
15		fveq1 5871	. . . . . . . . 9 |- ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
16	15	eqeq1d 2469	. . . . . . . 8 |- ( w = x -> ( ( w ` 0 ) = X <-> ( x ` 0 ) = X ) )
17		fveq1 5871	. . . . . . . . 9 |- ( w = x -> ( w ` ( ( N + 2 ) - 2 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
18	17, 15	neeq12d 2746	. . . . . . . 8 |- ( w = x -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) )
19	16, 18	anbi12d 710	. . . . . . 7 |- ( w = x -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
20	19	elrab 3266	. . . . . 6 |- ( x e. { w e. ( C ` ( N + 2 ) ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } <-> ( x e. ( C ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
21	14, 20	syl6bb 261	. . . . 5 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> ( x e. ( C ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
22	4	3ad2ant3 1019	. . . . . . . 8 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( N + 2 ) e. NN0 )
23	7	numclwwlkfvc 24901	. . . . . . . . 9 |- ( ( N + 2 ) e. NN0 -> ( C ` ( N + 2 ) ) = ( ( V ClWWalksN E ) ` ( N + 2 ) ) )
24	23	eleq2d 2537	. . . . . . . 8 |- ( ( N + 2 ) e. NN0 -> ( x e. ( C ` ( N + 2 ) ) <-> x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) ) )
25	22, 24	syl 16	. . . . . . 7 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( x e. ( C ` ( N + 2 ) ) <-> x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) ) )
26	25	anbi1d 704	. . . . . 6 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( x e. ( C ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) <-> ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
27		peano2nn 10560	. . . . . . . . . . . . 13 |- ( N e. NN -> ( N + 1 ) e. NN )
28		nnz 10898	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> N e. ZZ )
29		2z 10908	. . . . . . . . . . . . . . . . 17 |- 2 e. ZZ
30	29	a1i 11	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> 2 e. ZZ )
31	28, 30	zaddcld 10982	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N + 2 ) e. ZZ )
32		uzid 11108	. . . . . . . . . . . . . . 15 |- ( ( N + 2 ) e. ZZ -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
33	31, 32	syl 16	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
34		nncn 10556	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> N e. CC )
35		ax-1cn 9562	. . . . . . . . . . . . . . . . . 18 |- 1 e. CC
36	35	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> 1 e. CC )
37	34, 36, 36	addassd 9630	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
38		1p1e2 10661	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
39	38	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> ( 1 + 1 ) = 2 )
40	39	oveq2d 6311	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
41	37, 40	eqtrd 2508	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
42	41	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( ZZ>= ` ( ( N + 1 ) + 1 ) ) = ( ZZ>= ` ( N + 2 ) ) )
43	33, 42	eleqtrrd 2558	. . . . . . . . . . . . 13 |- ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) )
44	27, 43	jca 532	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
45	44	3ad2ant3 1019	. . . . . . . . . . 11 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
46	45	adantr 465	. . . . . . . . . 10 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
47		simprl 755	. . . . . . . . . 10 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) )
48		wwlksubclwwlk 24627	. . . . . . . . . 10 |- ( ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) -> ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) -> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) ) )
49	46, 47, 48	sylc 60	. . . . . . . . 9 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) )
50		pncan1 9995	. . . . . . . . . . . . . . 15 |- ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
51	50	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( N e. CC -> N = ( ( N + 1 ) - 1 ) )
52	34, 51	syl 16	. . . . . . . . . . . . 13 |- ( N e. NN -> N = ( ( N + 1 ) - 1 ) )
53	52	fveq2d 5876	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( V WWalksN E ) ` N ) = ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) )
54	53	eleq2d 2537	. . . . . . . . . . 11 |- ( N e. NN -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) <-> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) ) )
55	54	3ad2ant3 1019	. . . . . . . . . 10 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) <-> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) ) )
56	55	adantr 465	. . . . . . . . 9 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) <-> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) ) )
57	49, 56	mpbird 232	. . . . . . . 8 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) )
58		clwwlknprop 24595	. . . . . . . . . . . . 13 |- ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) -> ( ( V e. _V /\ E e. _V ) /\ x e. Word V /\ ( ( N + 2 ) e. NN0 /\ ( # ` x ) = ( N + 2 ) ) ) )
59		simprl 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( x ` 0 ) = X )
60		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> x e. Word V )
61		peano2nn0 10848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
62	1, 61	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( N + 1 ) e. NN0 )
63		nnre 10555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> N e. RR )
64	63	lep1d 10489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> N <_ ( N + 1 ) )
65		elfz2nn0 11780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. ( 0 ... ( N + 1 ) ) <-> ( N e. NN0 /\ ( N + 1 ) e. NN0 /\ N <_ ( N + 1 ) ) )
66	1, 62, 64, 65	syl3anbrc 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. NN -> N e. ( 0 ... ( N + 1 ) ) )
67		2cnd 10620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> 2 e. CC )
68		addsubass 9842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
69		2m1e1 10662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 2 - 1 ) = 1
70	69	oveq2i 6306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N + ( 2 - 1 ) ) = ( N + 1 )
71	68, 70	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
72	34, 67, 36, 71	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
73	72	oveq2d 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. NN -> ( 0 ... ( ( N + 2 ) - 1 ) ) = ( 0 ... ( N + 1 ) ) )
74	66, 73	eleqtrrd 2558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. NN -> N e. ( 0 ... ( ( N + 2 ) - 1 ) ) )
75		elfzp1b 11767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. ZZ /\ ( N + 2 ) e. ZZ ) -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
76	28, 31, 75	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. NN -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
77	74, 76	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. NN -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
78	77	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
79		oveq2 6303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( # ` x ) = ( N + 2 ) -> ( 1 ... ( # ` x ) ) = ( 1 ... ( N + 2 ) ) )
80	79	eleq2d 2537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( # ` x ) = ( N + 2 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
81	80	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
82	78, 81	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( # ` x ) ) )
83		swrd0fv0 12647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
84	60, 82, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
85	84	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) ) )
86	85	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) ) )
87	86	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
88	87	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
89		simpl 457	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( x ` 0 ) = X )
90	88, 89	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X )
91		swrd0fvlsw 12650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
92	60, 82, 91	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
93	34, 50	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
94	34, 67	pncand 9943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. NN -> ( ( N + 2 ) - 2 ) = N )
95	93, 94	eqtr4d 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> ( ( N + 1 ) - 1 ) = ( ( N + 2 ) - 2 ) )
96	95	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
97	96	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
98	92, 97	eqtr2d 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
99	98	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) ) )
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) ) )
101	100	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
102	101	neeq1d 2744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
103	102	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) -> ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
104	103	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
105	104	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) )
106	105	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) )
107		neeq2 2750	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( X = ( x ` 0 ) -> ( ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
108	107	eqcoms 2479	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x ` 0 ) = X -> ( ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
109	108	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
110	106, 109	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X )
111	90, 110	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( x ` 0 ) = X /\ ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) )
112	59, 111	mpancom 669	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) )
113	112	exp31 604	. . . . . . . . . . . . . . . . . 18 |- ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
114	113	com23 78	. . . . . . . . . . . . . . . . 17 |- ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
115	114	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( # ` x ) = ( N + 2 ) -> ( x e. Word V -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) ) )
116	115	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( ( N + 2 ) e. NN0 /\ ( # ` x ) = ( N + 2 ) ) -> ( x e. Word V -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) ) )
117	116	impcom 430	. . . . . . . . . . . . . 14 |- ( ( x e. Word V /\ ( ( N + 2 ) e. NN0 /\ ( # ` x ) = ( N + 2 ) ) ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
118	117	3adant1 1014	. . . . . . . . . . . . 13 |- ( ( ( V e. _V /\ E e. _V ) /\ x e. Word V /\ ( ( N + 2 ) e. NN0 /\ ( # ` x ) = ( N + 2 ) ) ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
119	58, 118	syl 16	. . . . . . . . . . . 12 |- ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) -> ( ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
120	119	imp 429	. . . . . . . . . . 11 |- ( ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( X e. V /\ N e. NN ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
121	120	com12 31	. . . . . . . . . 10 |- ( ( X e. V /\ N e. NN ) -> ( ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
122	121	3adant1 1014	. . . . . . . . 9 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
123	122	imp 429	. . . . . . . 8 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) )
124	57, 123	jca 532	. . . . . . 7 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
125	124	ex 434	. . . . . 6 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
126	26, 125	sylbid 215	. . . . 5 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( x e. ( C ` ( N + 2 ) ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
127	21, 126	sylbid 215	. . . 4 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
128	127	imp 429	. . 3 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
129	1	anim2i 569	. . . . . . . 8 |- ( ( X e. V /\ N e. NN ) -> ( X e. V /\ N e. NN0 ) )
130	129	3adant1 1014	. . . . . . 7 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( X e. V /\ N e. NN0 ) )
131	130	adantr 465	. . . . . 6 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( X e. V /\ N e. NN0 ) )
132	7, 8, 9, 10	numclwwlkovq 24923	. . . . . 6 |- ( ( X e. V /\ N e. NN0 ) -> ( X Q N ) = { w e. ( ( V WWalksN E ) ` N ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
133	131, 132	syl 16	. . . . 5 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( X Q N ) = { w e. ( ( V WWalksN E ) ` N ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
134	133	eleq2d 2537	. . . 4 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( X Q N ) <-> ( x substr <. 0 , ( N + 1 ) >. ) e. { w e. ( ( V WWalksN E ) ` N ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
135		fveq1 5871	. . . . . . 7 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( w ` 0 ) = ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) )
136	135	eqeq1d 2469	. . . . . 6 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( ( w ` 0 ) = X <-> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X ) )
137		fveq2 5872	. . . . . . 7 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( lastS ` w ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
138	137	neeq1d 2744	. . . . . 6 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( ( lastS ` w ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) )
139	136, 138	anbi12d 710	. . . . 5 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) <-> ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
140	139	elrab 3266	. . . 4 |- ( ( x substr <. 0 , ( N + 1 ) >. ) e. { w e. ( ( V WWalksN E ) ` N ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } <-> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) )
141	134, 140	syl6bb 261	. . 3 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( X Q N ) <-> ( ( x substr <. 0 , ( N + 1 ) >. ) e. ( ( V WWalksN E ) ` N ) /\ ( ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X /\ ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) ) ) )
142	128, 141	mpbird 232	. 2 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( x substr <. 0 , ( N + 1 ) >. ) e. ( X Q N ) )
143		numclwwlk.r	. 2 |- R = ( x e. ( X H ( N + 2 ) ) |-> ( x substr <. 0 , ( N + 1 ) >. ) )
144	142, 143	fmptd 6056	1 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   {crab 2821   _Vcvv 3118   <.cop 4039   class class class wbr 4453   |-> cmpt 4511   -->wf 5590   ` cfv 5594  (class class class)co 6295   |-> cmpt2 6297   CCcc 9502   0cc0 9504   1c1 9505   + caddc 9507   <_ cle 9641   - cmin 9817   NNcn 10548   2c2 10597   NN0cn0 10807   ZZcz 10876   ZZ>=cuz 11094   ...cfz 11684   #chash 12385  Word cword 12515   lastS clsw 12516   substr csubstr 12519   WWalksN cwwlkn 24501   ClWWalksN cclwwlkn 24572   FriendGrph cfrgra 24811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-1o 7142  df-oadd 7146  df-er 7323  df-map 7434  df-pm 7435  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-card 8332  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-nn 10549  df-2 10606  df-n0 10808  df-z 10877  df-uz 11095  df-fz 11685  df-fzo 11805  df-hash 12386  df-word 12523  df-lsw 12524  df-substr 12527  df-wwlk 24502  df-wwlkn 24503  df-clwwlk 24574  df-clwwlkn 24575

This theorem is referenced by:  numclwlk2lem2f1o  24929