numclwwlk2lem1

Description: In a friendship graph, for each walk of length n starting at a fixed vertex v and ending not at this vertex, there is a unique vertex so that the walk extended by an edge to this vertex and an edge from this vertex to the first vertex of the walk is a value of operation H . If the walk is represented as a word, it is sufficient to add one vertex to the word to obtain the closed walk contained in the value of operation H , since in a word representing a closed walk the starting vertex is not repeated at the end. This theorem generally holds only for friendship graphs, because these guarantee that for the first and last vertex there is a (unique) third vertex "in between". (Contributed by Alexander van der Vekens, 3-Oct-2018) (Revised by AV, 30-May-2021) (Revised by AV, 1-May-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\})$
Assertion	numclwwlk2lem1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (W \in (X Q N) \to \exists! v \in V W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$

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	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)\}$
5	4	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
6	5	eleq2d	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (W \in (X Q N) \leftrightarrow W \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\})$
7		fveq1	$⊢ w = W \to w (0) = W (0)$
8	7	eqeq1d	$⊢ w = W \to (w (0) = X \leftrightarrow W (0) = X)$
9		fveq2	$⊢ w = W \to lastS (w) = lastS (W)$
10	9	neeq1d	$⊢ w = W \to (lastS (w) \neq X \leftrightarrow lastS (W) \neq X)$
11	8 10	anbi12d	$⊢ w = W \to ((w (0) = X \land lastS (w) \neq X) \leftrightarrow (W (0) = X \land lastS (W) \neq X))$
12	11	elrab	$⊢ W \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\} \leftrightarrow (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))$
13	6 12	bitrdi	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (W \in (X Q N) \leftrightarrow (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)))$
14		simpl1	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to G \in FriendGraph$
15		eqid	$⊢ Edg (G) = Edg (G)$
16	1 15	wwlknp	$⊢ W \in (N WWalksN G) \to (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in Edg (G))$
17		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
18	17	adantl	$⊢ ((W \in Word V \land \|W\| = N + 1) \land N \in ℕ) \to N + 1 \in ℕ$
19		simpl	$⊢ ((W \in Word V \land \|W\| = N + 1) \land N \in ℕ) \to (W \in Word V \land \|W\| = N + 1)$
20	18 19	jca	$⊢ ((W \in Word V \land \|W\| = N + 1) \land N \in ℕ) \to (N + 1 \in ℕ \land (W \in Word V \land \|W\| = N + 1))$
21	20	ex	$⊢ (W \in Word V \land \|W\| = N + 1) \to (N \in ℕ \to (N + 1 \in ℕ \land (W \in Word V \land \|W\| = N + 1)))$
22	21	3adant3	$⊢ (W \in Word V \land \|W\| = N + 1 \land \forall i \in (0 ..^N) \{W (i), W (i + 1)\} \in Edg (G)) \to (N \in ℕ \to (N + 1 \in ℕ \land (W \in Word V \land \|W\| = N + 1)))$
23	16 22	syl	$⊢ W \in (N WWalksN G) \to (N \in ℕ \to (N + 1 \in ℕ \land (W \in Word V \land \|W\| = N + 1)))$
24		lswlgt0cl	$⊢ (N + 1 \in ℕ \land (W \in Word V \land \|W\| = N + 1)) \to lastS (W) \in V$
25	23 24	syl6	$⊢ W \in (N WWalksN G) \to (N \in ℕ \to lastS (W) \in V)$
26	25	adantr	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to (N \in ℕ \to lastS (W) \in V)$
27	26	com12	$⊢ N \in ℕ \to ((W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to lastS (W) \in V)$
28	27	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to lastS (W) \in V)$
29	28	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to lastS (W) \in V$
30		eleq1	$⊢ W (0) = X \to (W (0) \in V \leftrightarrow X \in V)$
31	30	biimprd	$⊢ W (0) = X \to (X \in V \to W (0) \in V)$
32	31	ad2antrl	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to (X \in V \to W (0) \in V)$
33	32	com12	$⊢ X \in V \to ((W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to W (0) \in V)$
34	33	3ad2ant2	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to W (0) \in V)$
35	34	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to W (0) \in V$
36		neeq2	$⊢ X = W (0) \to (lastS (W) \neq X \leftrightarrow lastS (W) \neq W (0))$
37	36	eqcoms	$⊢ W (0) = X \to (lastS (W) \neq X \leftrightarrow lastS (W) \neq W (0))$
38	37	biimpa	$⊢ (W (0) = X \land lastS (W) \neq X) \to lastS (W) \neq W (0)$
39	38	adantl	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to lastS (W) \neq W (0)$
40	39	adantl	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to lastS (W) \neq W (0)$
41	29 35 40	3jca	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to (lastS (W) \in V \land W (0) \in V \land lastS (W) \neq W (0))$
42	1 15	frcond2	$⊢ G \in FriendGraph \to ((lastS (W) \in V \land W (0) \in V \land lastS (W) \neq W (0)) \to \exists! v \in V (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)))$
43	14 41 42	sylc	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to \exists! v \in V (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G))$
44		simpl	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to W \in (N WWalksN G)$
45	44	ad2antlr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to W \in (N WWalksN G)$
46		simpr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to v \in V$
47		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
48	47	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to N \in ℕ_{0}$
49	48	ad2antrr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to N \in ℕ_{0}$
50	45 46 49	3jca	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W \in (N WWalksN G) \land v \in V \land N \in ℕ_{0})$
51	1 15	wwlksext2clwwlk	$⊢ (W \in (N WWalksN G) \land v \in V) \to ((\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)) \to W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G))$
52	51	3adant3	$⊢ (W \in (N WWalksN G) \land v \in V \land N \in ℕ_{0}) \to ((\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)) \to W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G))$
53	52	imp	$⊢ ((W \in (N WWalksN G) \land v \in V \land N \in ℕ_{0}) \land (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G))) \to W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)$
54	50 53	sylan	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G))) \to W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)$
55	1	wwlknbp	$⊢ W \in (N WWalksN G) \to (G \in V \land N \in ℕ_{0} \land W \in Word V)$
56	55	simp3d	$⊢ W \in (N WWalksN G) \to W \in Word V$
57	56	ad2antrl	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to W \in Word V$
58	57	ad2antrr	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to W \in Word V$
59	46	adantr	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to v \in V$
60		2z	$⊢ 2 \in ℤ$
61		nn0pzuz	$⊢ (N \in ℕ_{0} \land 2 \in ℤ) \to N + 2 \in ℤ_{\geq 2}$
62	47 60 61	sylancl	$⊢ N \in ℕ \to N + 2 \in ℤ_{\geq 2}$
63	62	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to N + 2 \in ℤ_{\geq 2}$
64	63	ad3antrrr	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to N + 2 \in ℤ_{\geq 2}$
65		simpr	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)$
66	1 15	clwwlkext2edg	$⊢ ((W \in Word V \land v \in V \land N + 2 \in ℤ_{\geq 2}) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G))$
67	58 59 64 65 66	syl31anc	$⊢ ((((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \land W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G)) \to (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G))$
68	54 67	impbida	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)) \leftrightarrow W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G))$
69	46 1	eleqtrdi	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to v \in Vtx (G)$
70	38	anim2i	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to (W \in (N WWalksN G) \land lastS (W) \neq W (0))$
71	70	ad2antlr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W \in (N WWalksN G) \land lastS (W) \neq W (0))$
72	71	simprd	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to lastS (W) \neq W (0)$
73		numclwwlk2lem1lem	$⊢ (v \in Vtx (G) \land W \in (N WWalksN G) \land lastS (W) \neq W (0)) \to ((W ++ ⟨“ v ”⟩) (0) = W (0) \land (W ++ ⟨“ v ”⟩) (N) \neq W (0))$
74	69 45 72 73	syl3anc	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (0) = W (0) \land (W ++ ⟨“ v ”⟩) (N) \neq W (0))$
75		eqeq2	$⊢ X = W (0) \to ((W ++ ⟨“ v ”⟩) (0) = X \leftrightarrow (W ++ ⟨“ v ”⟩) (0) = W (0))$
76	75	eqcoms	$⊢ W (0) = X \to ((W ++ ⟨“ v ”⟩) (0) = X \leftrightarrow (W ++ ⟨“ v ”⟩) (0) = W (0))$
77	76	ad2antrl	$⊢ (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to ((W ++ ⟨“ v ”⟩) (0) = X \leftrightarrow (W ++ ⟨“ v ”⟩) (0) = W (0))$
78	77	ad2antlr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (0) = X \leftrightarrow (W ++ ⟨“ v ”⟩) (0) = W (0))$
79	74	simpld	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W ++ ⟨“ v ”⟩) (0) = W (0)$
80	79	neeq2d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (N) \neq (W ++ ⟨“ v ”⟩) (0) \leftrightarrow (W ++ ⟨“ v ”⟩) (N) \neq W (0))$
81	78 80	anbi12d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N) \neq (W ++ ⟨“ v ”⟩) (0)) \leftrightarrow ((W ++ ⟨“ v ”⟩) (0) = W (0) \land (W ++ ⟨“ v ”⟩) (N) \neq W (0)))$
82	74 81	mpbird	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N) \neq (W ++ ⟨“ v ”⟩) (0))$
83		nncn	$⊢ N \in ℕ \to N \in ℂ$
84		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
85	83 84	pncand	$⊢ N \in ℕ \to N + 2 - 2 = N$
86	85	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to N + 2 - 2 = N$
87	86	ad2antrr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to N + 2 - 2 = N$
88	87	fveq2d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W ++ ⟨“ v ”⟩) (N + 2 - 2) = (W ++ ⟨“ v ”⟩) (N)$
89	88	neeq1d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0) \leftrightarrow (W ++ ⟨“ v ”⟩) (N) \neq (W ++ ⟨“ v ”⟩) (0))$
90	89	anbi2d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0)) \leftrightarrow ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N) \neq (W ++ ⟨“ v ”⟩) (0)))$
91	82 90	mpbird	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0))$
92	91	biantrud	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G) \leftrightarrow (W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G) \land ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0))))$
93	62	anim2i	$⊢ (X \in V \land N \in ℕ) \to (X \in V \land N + 2 \in ℤ_{\geq 2})$
94	93	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (X \in V \land N + 2 \in ℤ_{\geq 2})$
95	94	ad2antrr	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (X \in V \land N + 2 \in ℤ_{\geq 2})$
96	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))\}$
97	95 96	syl	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to X H (N + 2) = \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\}$
98	97	eleq2d	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to (W ++ ⟨“ v ”⟩ \in (X H (N + 2)) \leftrightarrow W ++ ⟨“ v ”⟩ \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\})$
99		fveq1	$⊢ w = W ++ ⟨“ v ”⟩ \to w (0) = (W ++ ⟨“ v ”⟩) (0)$
100	99	eqeq1d	$⊢ w = W ++ ⟨“ v ”⟩ \to (w (0) = X \leftrightarrow (W ++ ⟨“ v ”⟩) (0) = X)$
101		fveq1	$⊢ w = W ++ ⟨“ v ”⟩ \to w (N + 2 - 2) = (W ++ ⟨“ v ”⟩) (N + 2 - 2)$
102	101 99	neeq12d	$⊢ w = W ++ ⟨“ v ”⟩ \to (w (N + 2 - 2) \neq w (0) \leftrightarrow (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0))$
103	100 102	anbi12d	$⊢ w = W ++ ⟨“ v ”⟩ \to ((w (0) = X \land w (N + 2 - 2) \neq w (0)) \leftrightarrow ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0)))$
104	103	elrab	$⊢ W ++ ⟨“ v ”⟩ \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\} \leftrightarrow (W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G) \land ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0)))$
105	98 104	bitr2di	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((W ++ ⟨“ v ”⟩ \in ((N + 2) ClWWalksN G) \land ((W ++ ⟨“ v ”⟩) (0) = X \land (W ++ ⟨“ v ”⟩) (N + 2 - 2) \neq (W ++ ⟨“ v ”⟩) (0))) \leftrightarrow W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$
106	68 92 105	3bitrd	$⊢ (((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \land v \in V) \to ((\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)) \leftrightarrow W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$
107	106	reubidva	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to (\exists! v \in V (\{lastS (W), v\} \in Edg (G) \land \{v, W (0)\} \in Edg (G)) \leftrightarrow \exists! v \in V W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$
108	43 107	mpbid	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land (W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X))) \to \exists! v \in V W ++ ⟨“ v ”⟩ \in (X H (N + 2))$
109	108	ex	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((W \in (N WWalksN G) \land (W (0) = X \land lastS (W) \neq X)) \to \exists! v \in V W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$
110	13 109	sylbid	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (W \in (X Q N) \to \exists! v \in V W ++ ⟨“ v ”⟩ \in (X H (N + 2)))$

Metamath Proof Explorer

Theorem numclwwlk2lem1

Proof