numclwlk2lem2f

Description: R is a function mapping the "closed (n+2)-walks v(0) ... v(n-2) v(n-1) v(n) v(n+1) v(n+2) starting at X = v(0) = v(n+2) with v(n) =/= X" to the words representing the prefix v(0) ... v(n-2) v(n-1) v(n) of the walk. (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 31-May-2021) (Proof shortened by AV, 23-Mar-2022) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	numclwwlk.v	$⊢ V = Vtx (G)$
	numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
	numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
	numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
Assertion	numclwlk2lem2f	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to R : X H (N + 2) ⟶ X Q N$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	$⊢ V = Vtx (G)$
2		numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
3		numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
4		numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
5		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
6		2z	$⊢ 2 \in ℤ$
7	6	a1i	$⊢ N \in ℕ \to 2 \in ℤ$
8		nn0pzuz	$⊢ (N \in ℕ_{0} \land 2 \in ℤ) \to N + 2 \in ℤ_{\geq 2}$
9	5 7 8	syl2anc	$⊢ N \in ℕ \to N + 2 \in ℤ_{\geq 2}$
10	9	anim2i	$⊢ (X \in V \land N \in ℕ) \to (X \in V \land N + 2 \in ℤ_{\geq 2})$
11	10	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (X \in V \land N + 2 \in ℤ_{\geq 2})$
12	3	numclwwlkovh	$⊢ (X \in V \land N + 2 \in ℤ_{\geq 2}) \to X H (N + 2) = \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\}$
13	12	eleq2d	$⊢ (X \in V \land N + 2 \in ℤ_{\geq 2}) \to (x \in (X H (N + 2)) \leftrightarrow x \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\})$
14	11 13	syl	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \leftrightarrow x \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\})$
15		fveq1	$⊢ w = x \to w (0) = x (0)$
16	15	eqeq1d	$⊢ w = x \to (w (0) = X \leftrightarrow x (0) = X)$
17		fveq1	$⊢ w = x \to w (N + 2 - 2) = x (N + 2 - 2)$
18	17 15	neeq12d	$⊢ w = x \to (w (N + 2 - 2) \neq w (0) \leftrightarrow x (N + 2 - 2) \neq x (0))$
19	16 18	anbi12d	$⊢ w = x \to ((w (0) = X \land w (N + 2 - 2) \neq w (0)) \leftrightarrow (x (0) = X \land x (N + 2 - 2) \neq x (0)))$
20	19	elrab	$⊢ x \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\} \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))$
21	14 20	bitrdi	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))))$
22		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
23		nnz	$⊢ N \in ℕ \to N \in ℤ$
24	23 7	zaddcld	$⊢ N \in ℕ \to N + 2 \in ℤ$
25		uzid	$⊢ N + 2 \in ℤ \to N + 2 \in ℤ_{\geq (N + 2)}$
26	24 25	syl	$⊢ N \in ℕ \to N + 2 \in ℤ_{\geq (N + 2)}$
27		nncn	$⊢ N \in ℕ \to N \in ℂ$
28		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
29	27 28 28	addassd	$⊢ N \in ℕ \to N + 1 + 1 = N + 1 + 1$
30		1p1e2	$⊢ 1 + 1 = 2$
31	30	a1i	$⊢ N \in ℕ \to 1 + 1 = 2$
32	31	oveq2d	$⊢ N \in ℕ \to N + 1 + 1 = N + 2$
33	29 32	eqtrd	$⊢ N \in ℕ \to N + 1 + 1 = N + 2$
34	33	fveq2d	$⊢ N \in ℕ \to ℤ_{\geq (N + 1 + 1)} = ℤ_{\geq (N + 2)}$
35	26 34	eleqtrrd	$⊢ N \in ℕ \to N + 2 \in ℤ_{\geq (N + 1 + 1)}$
36	22 35	jca	$⊢ N \in ℕ \to (N + 1 \in ℕ \land N + 2 \in ℤ_{\geq (N + 1 + 1)})$
37	36	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (N + 1 \in ℕ \land N + 2 \in ℤ_{\geq (N + 1 + 1)})$
38	37	adantr	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (N + 1 \in ℕ \land N + 2 \in ℤ_{\geq (N + 1 + 1)})$
39		simprl	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to x \in ((N + 2) ClWWalksN G)$
40		wwlksubclwwlk	$⊢ (N + 1 \in ℕ \land N + 2 \in ℤ_{\geq (N + 1 + 1)}) \to (x \in ((N + 2) ClWWalksN G) \to x prefix (N + 1) \in ((N + 1 - 1) WWalksN G))$
41	38 39 40	sylc	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to x prefix (N + 1) \in ((N + 1 - 1) WWalksN G)$
42		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
43	42	eqcomd	$⊢ N \in ℂ \to N = N + 1 - 1$
44	27 43	syl	$⊢ N \in ℕ \to N = N + 1 - 1$
45	44	oveq1d	$⊢ N \in ℕ \to N WWalksN G = (N + 1 - 1) WWalksN G$
46	45	eleq2d	$⊢ N \in ℕ \to (x prefix (N + 1) \in (N WWalksN G) \leftrightarrow x prefix (N + 1) \in ((N + 1 - 1) WWalksN G))$
47	46	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x prefix (N + 1) \in (N WWalksN G) \leftrightarrow x prefix (N + 1) \in ((N + 1 - 1) WWalksN G))$
48	47	adantr	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (x prefix (N + 1) \in (N WWalksN G) \leftrightarrow x prefix (N + 1) \in ((N + 1 - 1) WWalksN G))$
49	41 48	mpbird	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to x prefix (N + 1) \in (N WWalksN G)$
50	1	clwwlknbp	$⊢ x \in ((N + 2) ClWWalksN G) \to (x \in Word V \land \|x\| = N + 2)$
51		simprl	$⊢ (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to x (0) = X$
52		simprr	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to x \in Word V$
53		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
54	5 53	syl	$⊢ N \in ℕ \to N + 1 \in ℕ_{0}$
55		nnre	$⊢ N \in ℕ \to N \in ℝ$
56	55	lep1d	$⊢ N \in ℕ \to N \leq N + 1$
57		elfz2nn0	$⊢ N \in (0 \dots N + 1) \leftrightarrow (N \in ℕ_{0} \land N + 1 \in ℕ_{0} \land N \leq N + 1)$
58	5 54 56 57	syl3anbrc	$⊢ N \in ℕ \to N \in (0 \dots N + 1)$
59		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
60		addsubass	$⊢ (N \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to N + 2 - 1 = N + 2 - 1$
61		2m1e1	$⊢ 2 - 1 = 1$
62	61	oveq2i	$⊢ N + 2 - 1 = N + 1$
63	60 62	eqtrdi	$⊢ (N \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \to N + 2 - 1 = N + 1$
64	27 59 28 63	syl3anc	$⊢ N \in ℕ \to N + 2 - 1 = N + 1$
65	64	oveq2d	$⊢ N \in ℕ \to (0 \dots N + 2 - 1) = (0 \dots N + 1)$
66	58 65	eleqtrrd	$⊢ N \in ℕ \to N \in (0 \dots N + 2 - 1)$
67		elfzp1b	$⊢ (N \in ℤ \land N + 2 \in ℤ) \to (N \in (0 \dots N + 2 - 1) \leftrightarrow N + 1 \in (1 \dots N + 2))$
68	23 24 67	syl2anc	$⊢ N \in ℕ \to (N \in (0 \dots N + 2 - 1) \leftrightarrow N + 1 \in (1 \dots N + 2))$
69	66 68	mpbid	$⊢ N \in ℕ \to N + 1 \in (1 \dots N + 2)$
70	69	adantr	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to N + 1 \in (1 \dots N + 2)$
71		oveq2	$⊢ \|x\| = N + 2 \to (1 \dots \|x\|) = (1 \dots N + 2)$
72	71	eleq2d	$⊢ \|x\| = N + 2 \to (N + 1 \in (1 \dots \|x\|) \leftrightarrow N + 1 \in (1 \dots N + 2))$
73	72	ad2antrl	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to (N + 1 \in (1 \dots \|x\|) \leftrightarrow N + 1 \in (1 \dots N + 2))$
74	70 73	mpbird	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to N + 1 \in (1 \dots \|x\|)$
75		pfxfv0	$⊢ (x \in Word V \land N + 1 \in (1 \dots \|x\|)) \to (x prefix (N + 1)) (0) = x (0)$
76	52 74 75	syl2anc	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to (x prefix (N + 1)) (0) = x (0)$
77	76	ex	$⊢ N \in ℕ \to ((\|x\| = N + 2 \land x \in Word V) \to (x prefix (N + 1)) (0) = x (0))$
78	77	adantl	$⊢ (X \in V \land N \in ℕ) \to ((\|x\| = N + 2 \land x \in Word V) \to (x prefix (N + 1)) (0) = x (0))$
79	78	impcom	$⊢ ((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \to (x prefix (N + 1)) (0) = x (0)$
80	79	ad2antrl	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (x prefix (N + 1)) (0) = x (0)$
81		simpl	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to x (0) = X$
82	80 81	eqtrd	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (x prefix (N + 1)) (0) = X$
83		pfxfvlsw	$⊢ (x \in Word V \land N + 1 \in (1 \dots \|x\|)) \to lastS (x prefix (N + 1)) = x (N + 1 - 1)$
84	52 74 83	syl2anc	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to lastS (x prefix (N + 1)) = x (N + 1 - 1)$
85	27 42	syl	$⊢ N \in ℕ \to N + 1 - 1 = N$
86	27 59	pncand	$⊢ N \in ℕ \to N + 2 - 2 = N$
87	85 86	eqtr4d	$⊢ N \in ℕ \to N + 1 - 1 = N + 2 - 2$
88	87	fveq2d	$⊢ N \in ℕ \to x (N + 1 - 1) = x (N + 2 - 2)$
89	88	adantr	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to x (N + 1 - 1) = x (N + 2 - 2)$
90	84 89	eqtr2d	$⊢ (N \in ℕ \land (\|x\| = N + 2 \land x \in Word V)) \to x (N + 2 - 2) = lastS (x prefix (N + 1))$
91	90	ex	$⊢ N \in ℕ \to ((\|x\| = N + 2 \land x \in Word V) \to x (N + 2 - 2) = lastS (x prefix (N + 1)))$
92	91	adantl	$⊢ (X \in V \land N \in ℕ) \to ((\|x\| = N + 2 \land x \in Word V) \to x (N + 2 - 2) = lastS (x prefix (N + 1)))$
93	92	impcom	$⊢ ((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \to x (N + 2 - 2) = lastS (x prefix (N + 1))$
94	93	neeq1d	$⊢ ((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \to (x (N + 2 - 2) \neq x (0) \leftrightarrow lastS (x prefix (N + 1)) \neq x (0))$
95	94	biimpcd	$⊢ x (N + 2 - 2) \neq x (0) \to (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \to lastS (x prefix (N + 1)) \neq x (0))$
96	95	adantl	$⊢ (x (0) = X \land x (N + 2 - 2) \neq x (0)) \to (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \to lastS (x prefix (N + 1)) \neq x (0))$
97	96	impcom	$⊢ (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to lastS (x prefix (N + 1)) \neq x (0)$
98	97	adantl	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to lastS (x prefix (N + 1)) \neq x (0)$
99		neeq2	$⊢ X = x (0) \to (lastS (x prefix (N + 1)) \neq X \leftrightarrow lastS (x prefix (N + 1)) \neq x (0))$
100	99	eqcoms	$⊢ x (0) = X \to (lastS (x prefix (N + 1)) \neq X \leftrightarrow lastS (x prefix (N + 1)) \neq x (0))$
101	100	adantr	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (lastS (x prefix (N + 1)) \neq X \leftrightarrow lastS (x prefix (N + 1)) \neq x (0))$
102	98 101	mpbird	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to lastS (x prefix (N + 1)) \neq X$
103	82 102	jca	$⊢ (x (0) = X \land (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)$
104	51 103	mpancom	$⊢ (((\|x\| = N + 2 \land x \in Word V) \land (X \in V \land N \in ℕ)) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)$
105	104	exp31	$⊢ (\|x\| = N + 2 \land x \in Word V) \to ((X \in V \land N \in ℕ) \to ((x (0) = X \land x (N + 2 - 2) \neq x (0)) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
106	105	com23	$⊢ (\|x\| = N + 2 \land x \in Word V) \to ((x (0) = X \land x (N + 2 - 2) \neq x (0)) \to ((X \in V \land N \in ℕ) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
107	106	ancoms	$⊢ (x \in Word V \land \|x\| = N + 2) \to ((x (0) = X \land x (N + 2 - 2) \neq x (0)) \to ((X \in V \land N \in ℕ) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
108	50 107	syl	$⊢ x \in ((N + 2) ClWWalksN G) \to ((x (0) = X \land x (N + 2 - 2) \neq x (0)) \to ((X \in V \land N \in ℕ) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
109	108	imp	$⊢ (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to ((X \in V \land N \in ℕ) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
110	109	com12	$⊢ (X \in V \land N \in ℕ) \to ((x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
111	110	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
112	111	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)$
113	49 112	jca	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))) \to (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
114	113	ex	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
115	21 114	sylbid	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \to (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
116	115	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
117		3simpc	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (X \in V \land N \in ℕ)$
118	117	adantr	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to (X \in V \land N \in ℕ)$
119	1 2	numclwwlkovq	$⊢ (X \in V \land N \in ℕ) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
120	118 119	syl	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
121	120	eleq2d	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to (x prefix (N + 1) \in (X Q N) \leftrightarrow x prefix (N + 1) \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\})$
122		fveq1	$⊢ w = x prefix (N + 1) \to w (0) = (x prefix (N + 1)) (0)$
123	122	eqeq1d	$⊢ w = x prefix (N + 1) \to (w (0) = X \leftrightarrow (x prefix (N + 1)) (0) = X)$
124		fveq2	$⊢ w = x prefix (N + 1) \to lastS (w) = lastS (x prefix (N + 1))$
125	124	neeq1d	$⊢ w = x prefix (N + 1) \to (lastS (w) \neq X \leftrightarrow lastS (x prefix (N + 1)) \neq X)$
126	123 125	anbi12d	$⊢ w = x prefix (N + 1) \to ((w (0) = X \land lastS (w) \neq X) \leftrightarrow ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
127	126	elrab	$⊢ x prefix (N + 1) \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\} \leftrightarrow (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X))$
128	121 127	bitrdi	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to (x prefix (N + 1) \in (X Q N) \leftrightarrow (x prefix (N + 1) \in (N WWalksN G) \land ((x prefix (N + 1)) (0) = X \land lastS (x prefix (N + 1)) \neq X)))$
129	116 128	mpbird	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to x prefix (N + 1) \in (X Q N)$
130	129 4	fmptd	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to R : X H (N + 2) ⟶ X Q N$

Metamath Proof Explorer

Theorem numclwlk2lem2f

Proof