Theorem numclwlk2lem2f 25684

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 10876	. . . . . . . . . 10 |- ( N e. NN -> N e. NN0 )
2		2nn0 10886	. . . . . . . . . . 11 |- 2 e. NN0
3	2	a1i 11	. . . . . . . . . 10 |- ( N e. NN -> 2 e. NN0 )
4	1, 3	nn0addcld 10929	. . . . . . . . 9 |- ( N e. NN -> ( N + 2 ) e. NN0 )
5	4	anim2i 571	. . . . . . . 8 |- ( ( X e. V /\ N e. NN ) -> ( X e. V /\ ( N + 2 ) e. NN0 ) )
6	5	3adant1 1023	. . . . . . 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 25682	. . . . . . . 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 2499	. . . . . . 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 17	. . . . . 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 5880	. . . . . . . . 9 |- ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
16	15	eqeq1d 2431	. . . . . . . 8 |- ( w = x -> ( ( w ` 0 ) = X <-> ( x ` 0 ) = X ) )
17		fveq1 5880	. . . . . . . . 9 |- ( w = x -> ( w ` ( ( N + 2 ) - 2 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
18	17, 15	neeq12d 2710	. . . . . . . 8 |- ( w = x -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) )
19	16, 18	anbi12d 715	. . . . . . 7 |- ( w = x -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
20	19	elrab 3235	. . . . . 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 264	. . . . 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 1028	. . . . . . . 8 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( N + 2 ) e. NN0 )
23	7	numclwwlkfvc 25658	. . . . . . . . 9 |- ( ( N + 2 ) e. NN0 -> ( C ` ( N + 2 ) ) = ( ( V ClWWalksN E ) ` ( N + 2 ) ) )
24	23	eleq2d 2499	. . . . . . . 8 |- ( ( N + 2 ) e. NN0 -> ( x e. ( C ` ( N + 2 ) ) <-> x e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) ) )
25	22, 24	syl 17	. . . . . . 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 709	. . . . . 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 10621	. . . . . . . . . . . . 13 |- ( N e. NN -> ( N + 1 ) e. NN )
28		nnz 10959	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> N e. ZZ )
29		2z 10969	. . . . . . . . . . . . . . . . 17 |- 2 e. ZZ
30	29	a1i 11	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> 2 e. ZZ )
31	28, 30	zaddcld 11044	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N + 2 ) e. ZZ )
32		uzid 11173	. . . . . . . . . . . . . . 15 |- ( ( N + 2 ) e. ZZ -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
33	31, 32	syl 17	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( N + 2 ) ) )
34		nncn 10617	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> N e. CC )
35		1cnd 9658	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> 1 e. CC )
36	34, 35, 35	addassd 9664	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
37		1p1e2 10723	. . . . . . . . . . . . . . . . . 18 |- ( 1 + 1 ) = 2
38	37	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( N e. NN -> ( 1 + 1 ) = 2 )
39	38	oveq2d 6321	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> ( N + ( 1 + 1 ) ) = ( N + 2 ) )
40	36, 39	eqtrd 2470	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + 2 ) )
41	40	fveq2d 5885	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( ZZ>= ` ( ( N + 1 ) + 1 ) ) = ( ZZ>= ` ( N + 2 ) ) )
42	33, 41	eleqtrrd 2520	. . . . . . . . . . . . 13 |- ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) )
43	27, 42	jca 534	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
44	43	3ad2ant3 1028	. . . . . . . . . . 11 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( ( N + 1 ) e. NN /\ ( N + 2 ) e. ( ZZ>= ` ( ( N + 1 ) + 1 ) ) ) )
45	44	adantr 466	. . . . . . . . . 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 ) ) ) )
46		simprl 762	. . . . . . . . . 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 ) ) )
47		wwlksubclwwlk 25385	. . . . . . . . . 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 ) ) ) )
48	45, 46, 47	sylc 62	. . . . . . . . 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 ) ) )
49		pncan1 10042	. . . . . . . . . . . . . . 15 |- ( N e. CC -> ( ( N + 1 ) - 1 ) = N )
50	49	eqcomd 2437	. . . . . . . . . . . . . 14 |- ( N e. CC -> N = ( ( N + 1 ) - 1 ) )
51	34, 50	syl 17	. . . . . . . . . . . . 13 |- ( N e. NN -> N = ( ( N + 1 ) - 1 ) )
52	51	fveq2d 5885	. . . . . . . . . . . 12 |- ( N e. NN -> ( ( V WWalksN E ) ` N ) = ( ( V WWalksN E ) ` ( ( N + 1 ) - 1 ) ) )
53	52	eleq2d 2499	. . . . . . . . . . 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 ) ) ) )
54	53	3ad2ant3 1028	. . . . . . . . . 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 ) ) ) )
55	54	adantr 466	. . . . . . . . 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 ) ) ) )
56	48, 55	mpbird 235	. . . . . . . 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 ) )
57		clwwlknprop 25353	. . . . . . . . . . . . 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 ) ) ) )
58		simprl 762	. . . . . . . . . . . . . . . . . . . 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 )
59		simprr 764	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> x e. Word V )
60		peano2nn0 10910	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN0 -> ( N + 1 ) e. NN0 )
61	1, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( N + 1 ) e. NN0 )
62		nnre 10616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> N e. RR )
63	62	lep1d 10538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> N <_ ( N + 1 ) )
64		elfz2nn0 11883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. ( 0 ... ( N + 1 ) ) <-> ( N e. NN0 /\ ( N + 1 ) e. NN0 /\ N <_ ( N + 1 ) ) )
65	1, 61, 63, 64	syl3anbrc 1189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. NN -> N e. ( 0 ... ( N + 1 ) ) )
66		2cnd 10682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> 2 e. CC )
67		addsubass 9884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + ( 2 - 1 ) ) )
68		2m1e1 10724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( 2 - 1 ) = 1
69	68	oveq2i 6316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N + ( 2 - 1 ) ) = ( N + 1 )
70	67, 69	syl6eq 2486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( N e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
71	34, 66, 35, 70	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( ( N + 2 ) - 1 ) = ( N + 1 ) )
72	71	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( N e. NN -> ( 0 ... ( ( N + 2 ) - 1 ) ) = ( 0 ... ( N + 1 ) ) )
73	65, 72	eleqtrrd 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. NN -> N e. ( 0 ... ( ( N + 2 ) - 1 ) ) )
74		elfzp1b 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. ZZ /\ ( N + 2 ) e. ZZ ) -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
75	28, 31, 74	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( N e. NN -> ( N e. ( 0 ... ( ( N + 2 ) - 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
76	73, 75	mpbid 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. NN -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
77	76	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) )
78		oveq2 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( # ` x ) = ( N + 2 ) -> ( 1 ... ( # ` x ) ) = ( 1 ... ( N + 2 ) ) )
79	78	eleq2d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( # ` x ) = ( N + 2 ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
80	79	ad2antrl 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( N + 1 ) e. ( 1 ... ( # ` x ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 2 ) ) ) )
81	77, 80	mpbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( N + 1 ) e. ( 1 ... ( # ` x ) ) )
82		swrd0fv0 12781	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
83	59, 81, 82	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
84	83	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) ) )
85	84	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) ) )
86	85	impcom 431	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( x ` 0 ) )
87	86	ad2antrl 732	. . . . . . . . . . . . . . . . . . . . . 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 ) )
88		simpl 458	. . . . . . . . . . . . . . . . . . . . . 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 )
89	87, 88	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . 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 )
90		swrd0fvlsw 12784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( x e. Word V /\ ( N + 1 ) e. ( 1 ... ( # ` x ) ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
91	59, 81, 90	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) = ( x ` ( ( N + 1 ) - 1 ) ) )
92	34, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
93	34, 66	pncand 9986	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( N e. NN -> ( ( N + 2 ) - 2 ) = N )
94	92, 93	eqtr4d 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( N e. NN -> ( ( N + 1 ) - 1 ) = ( ( N + 2 ) - 2 ) )
95	94	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( N e. NN -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
96	95	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 1 ) - 1 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
97	91, 96	eqtr2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( N e. NN /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
98	97	ex 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) ) )
99	98	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( X e. V /\ N e. NN ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) ) )
100	99	impcom 431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) /\ ( X e. V /\ N e. NN ) ) -> ( x ` ( ( N + 2 ) - 2 ) ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
101	100	neeq1d 2708	. . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
102	101	biimpcd 227	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
103	102	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
104	103	impcom 431	. . . . . . . . . . . . . . . . . . . . . . 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 ) )
105	104	adantl 467	. . . . . . . . . . . . . . . . . . . . . 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 ) )
106		neeq2 2714	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( X = ( x ` 0 ) -> ( ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
107	106	eqcoms 2441	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x ` 0 ) = X -> ( ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
108	107	adantr 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 <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= ( x ` 0 ) ) )
109	105, 108	mpbird 235	. . . . . . . . . . . . . . . . . . . . 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 )
110	89, 109	jca 534	. . . . . . . . . . . . . . . . . . . 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 ) )
111	58, 110	mpancom 673	. . . . . . . . . . . . . . . . . . 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 ) )
112	111	exp31 607	. . . . . . . . . . . . . . . . . 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 ) ) ) )
113	112	com23 81	. . . . . . . . . . . . . . . . 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 ) ) ) )
114	113	ex 435	. . . . . . . . . . . . . . . 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 ) ) ) ) )
115	114	adantl 467	. . . . . . . . . . . . . . 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 ) ) ) ) )
116	115	impcom 431	. . . . . . . . . . . . . 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 ) ) ) )
117	116	3adant1 1023	. . . . . . . . . . . . 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 ) ) ) )
118	57, 117	syl 17	. . . . . . . . . . . 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 ) ) ) )
119	118	imp 430	. . . . . . . . . . 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 ) ) )
120	119	com12 32	. . . . . . . . . 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 ) ) )
121	120	3adant1 1023	. . . . . . . . 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 ) ) )
122	121	imp 430	. . . . . . . 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 ) )
123	56, 122	jca 534	. . . . . . 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 ) ) )
124	123	ex 435	. . . . . 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 ) ) ) )
125	26, 124	sylbid 218	. . . . 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 ) ) ) )
126	21, 125	sylbid 218	. . . 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 ) ) ) )
127	126	imp 430	. . 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 ) ) )
128	1	anim2i 571	. . . . . . . 8 |- ( ( X e. V /\ N e. NN ) -> ( X e. V /\ N e. NN0 ) )
129	128	3adant1 1023	. . . . . . 7 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> ( X e. V /\ N e. NN0 ) )
130	129	adantr 466	. . . . . 6 |- ( ( ( V FriendGrph E /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( X e. V /\ N e. NN0 ) )
131	7, 8, 9, 10	numclwwlkovq 25680	. . . . . 6 |- ( ( X e. V /\ N e. NN0 ) -> ( X Q N ) = { w e. ( ( V WWalksN E ) ` N ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
132	130, 131	syl 17	. . . . 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 ) } )
133	132	eleq2d 2499	. . . 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 ) } ) )
134		fveq1 5880	. . . . . . 7 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( w ` 0 ) = ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) )
135	134	eqeq1d 2431	. . . . . 6 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( ( w ` 0 ) = X <-> ( ( x substr <. 0 , ( N + 1 ) >. ) ` 0 ) = X ) )
136		fveq2 5881	. . . . . . 7 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( lastS ` w ) = ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) )
137	136	neeq1d 2708	. . . . . 6 |- ( w = ( x substr <. 0 , ( N + 1 ) >. ) -> ( ( lastS ` w ) =/= X <-> ( lastS ` ( x substr <. 0 , ( N + 1 ) >. ) ) =/= X ) )
138	135, 137	anbi12d 715	. . . . 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 ) ) )
139	138	elrab 3235	. . . 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 ) ) )
140	133, 139	syl6bb 264	. . 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 ) ) ) )
141	127, 140	mpbird 235	. 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 ) )
142		numclwwlk.r	. 2 |- R = ( x e. ( X H ( N + 2 ) ) |-> ( x substr <. 0 , ( N + 1 ) >. ) )
143	141, 142	fmptd 6061	1 |- ( ( V FriendGrph E /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   =/= wne 2625   {crab 2786   _Vcvv 3087   <.cop 4008   class class class wbr 4426   |-> cmpt 4484   -->wf 5597   ` cfv 5601  (class class class)co 6305   |-> cmpt2 6307   CCcc 9536   0cc0 9538   1c1 9539   + caddc 9541   <_ cle 9675   - cmin 9859   NNcn 10609   2c2 10659   NN0cn0 10869   ZZcz 10937   ZZ>=cuz 11159   ...cfz 11782   #chash 12512  Word cword 12643   lastS clsw 12644   substr csubstr 12647   WWalksN cwwlkn 25259   ClWWalksN cclwwlkn 25330   FriendGrph cfrgra 25569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-map 7482  df-pm 7483  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-card 8372  df-cda 8596  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-fz 11783  df-fzo 11914  df-hash 12513  df-word 12651  df-lsw 12652  df-substr 12655  df-wwlk 25260  df-wwlkn 25261  df-clwwlk 25332  df-clwwlkn 25333

This theorem is referenced by:  numclwlk2lem2f1o  25686