numclwwlk2lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > numclwwlk2lem1		Structured version Visualization version GIF version

Theorem numclwwlk2lem1 30738

Description: In a friendship graph, for each walk of length 𝑛 starting at a fixed vertex 𝑣 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 𝐻. 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 𝐻, 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.)

**Hypotheses**
Ref	Expression
numclwwlk.v	⊢ 𝑉 = (Vtx‘𝐺)
numclwwlk.q	⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
numclwwlk.h	⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})

**Assertion**
Ref	Expression
numclwwlk2lem1	⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))

Distinct variable groups: 𝑛,𝐺,𝑣,𝑤 𝑛,𝑁,𝑣,𝑤 𝑛,𝑉,𝑣 𝑛,𝑋,𝑣,𝑤 𝑤,𝑉 𝑣,𝑊,𝑤 Allowed substitution hints: 𝑄(𝑤, 𝑣, 𝑛) 𝐻(𝑤, 𝑣, 𝑛) 𝑊(𝑛)

Proof of Theorem numclwwlk2lem1 Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		numclwwlk.v	. . . . . 6 ⊢ 𝑉 = (Vtx‘𝐺)
2		numclwwlk.q	. . . . . 6 ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})
3	1, 2	numclwwlkovq 30736	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})
4	3	3adant1 1147	. . . 4 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})
5	4	eleq2d 2848	. . 3 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ 𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)}))
6		fveq1 6880	. . . . . 6 ⊢ (𝑤 = 𝑊 → (𝑤‘0) = (𝑊‘0))
7	6	eqeq1d 2764	. . . . 5 ⊢ (𝑤 = 𝑊 → ((𝑤‘0) = 𝑋 ↔ (𝑊‘0) = 𝑋))
8		fveq2 6881	. . . . . 6 ⊢ (𝑤 = 𝑊 → (lastS‘𝑤) = (lastS‘𝑊))
9	8	neeq1d 3016	. . . . 5 ⊢ (𝑤 = 𝑊 → ((lastS‘𝑤) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ 𝑋))
10	7, 9	anbi12d 643	. . . 4 ⊢ (𝑤 = 𝑊 → (((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋) ↔ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)))
11	10	elrab 3649	. . 3 ⊢ (𝑊 ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)} ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)))
12	5, 11	bitrdi 290	. 2 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) ↔ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))))
13		simpl1 1209	. . . . 5 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → 𝐺 ∈ FriendGraph )
14		eqid 2762	. . . . . . . . . . . . 13 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
15	1, 14	wwlknp 30203	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
16		peano2nn 12251	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
17	16	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 1) ∈ ℕ)
18		simpl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)))
19	17, 18	jca 520	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))))
20	19	ex 417	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)))))
21	20	3adant3 1149	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)))))
22	15, 21	syl 18	. . . . . . . . . . 11 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)))))
23		lswlgt0cl 14613	. . . . . . . . . . 11 ⊢ (((𝑁 + 1) ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1))) → (lastS‘𝑊) ∈ 𝑉)
24	22, 23	syl6 36	. . . . . . . . . 10 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ → (lastS‘𝑊) ∈ 𝑉))
25	24	adantr 485	. . . . . . . . 9 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑁 ∈ ℕ → (lastS‘𝑊) ∈ 𝑉))
26	25	com12 33	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ∈ 𝑉))
27	26	3ad2ant3 1152	. . . . . . 7 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ∈ 𝑉))
28	27	imp 411	. . . . . 6 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (lastS‘𝑊) ∈ 𝑉)
29		eleq1 2850	. . . . . . . . . . 11 ⊢ ((𝑊‘0) = 𝑋 → ((𝑊‘0) ∈ 𝑉 ↔ 𝑋 ∈ 𝑉))
30	29	biimprd 251	. . . . . . . . . 10 ⊢ ((𝑊‘0) = 𝑋 → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉))
31	30	ad2antrl 740	. . . . . . . . 9 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑋 ∈ 𝑉 → (𝑊‘0) ∈ 𝑉))
32	31	com12 33	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑉 → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉))
33	32	3ad2ant2 1151	. . . . . . 7 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊‘0) ∈ 𝑉))
34	33	imp 411	. . . . . 6 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (𝑊‘0) ∈ 𝑉)
35		neeq2 3020	. . . . . . . . . 10 ⊢ (𝑋 = (𝑊‘0) → ((lastS‘𝑊) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ (𝑊‘0)))
36	35	eqcoms 2770	. . . . . . . . 9 ⊢ ((𝑊‘0) = 𝑋 → ((lastS‘𝑊) ≠ 𝑋 ↔ (lastS‘𝑊) ≠ (𝑊‘0)))
37	36	biimpa 481	. . . . . . . 8 ⊢ (((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋) → (lastS‘𝑊) ≠ (𝑊‘0))
38	37	adantl 486	. . . . . . 7 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (lastS‘𝑊) ≠ (𝑊‘0))
39	38	adantl 486	. . . . . 6 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (lastS‘𝑊) ≠ (𝑊‘0))
40	28, 34, 39	3jca 1145	. . . . 5 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → ((lastS‘𝑊) ∈ 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (lastS‘𝑊) ≠ (𝑊‘0)))
41	1, 14	frcond2 30629	. . . . 5 ⊢ (𝐺 ∈ FriendGraph → (((lastS‘𝑊) ∈ 𝑉 ∧ (𝑊‘0) ∈ 𝑉 ∧ (lastS‘𝑊) ≠ (𝑊‘0)) → ∃!𝑣 ∈ 𝑉 ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))))
42	13, 40, 41	sylc 66	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → ∃!𝑣 ∈ 𝑉 ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)))
43		simpl 487	. . . . . . . . . 10 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → 𝑊 ∈ (𝑁 WWalksN 𝐺))
44	43	ad2antlr 739	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑊 ∈ (𝑁 WWalksN 𝐺))
45		simpr 489	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉)
46		nnnn0 12517	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
47	46	3ad2ant3 1152	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑁 ∈ ℕ₀)
48	47	ad2antrr 738	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑁 ∈ ℕ₀)
49	44, 45, 48	3jca 1145	. . . . . . . 8 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀))
50	1, 14	wwlksext2clwwlk 30419	. . . . . . . . . 10 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))
51	50	3adant3 1149	. . . . . . . . 9 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) → (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))
52	51	imp 411	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑣 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) ∧ ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
53	49, 52	sylan 591	. . . . . . 7 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺))) → (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
54	1	wwlknbp 30202	. . . . . . . . . . 11 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word 𝑉))
55	54	simp3d 1161	. . . . . . . . . 10 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → 𝑊 ∈ Word 𝑉)
56	55	ad2antrl 740	. . . . . . . . 9 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → 𝑊 ∈ Word 𝑉)
57	56	ad2antrr 738	. . . . . . . 8 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑊 ∈ Word 𝑉)
58	45	adantr 485	. . . . . . . 8 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → 𝑣 ∈ 𝑉)
59		2z 12632	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
60		nn0pzuz 12935	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 2 ∈ ℤ) → (𝑁 + 2) ∈ (ℤ_≥‘2))
61	46, 59, 60	sylancl 597	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈ (ℤ_≥‘2))
62	61	3ad2ant3 1152	. . . . . . . . 9 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) ∈ (ℤ_≥‘2))
63	62	ad3antrrr 742	. . . . . . . 8 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑁 + 2) ∈ (ℤ_≥‘2))
64		simpr 489	. . . . . . . 8 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
65	1, 14	clwwlkext2edg 30418	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑣 ∈ 𝑉 ∧ (𝑁 + 2) ∈ (ℤ_≥‘2)) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)))
66	57, 58, 63, 64, 65	syl31anc 1399	. . . . . . 7 ⊢ (((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) ∧ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)))
67	53, 66	impbida 812	. . . . . 6 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))
68	45, 1	eleqtrdi 2872	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ (Vtx‘𝐺))
69	37	anim2i 628	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0)))
70	69	ad2antlr 739	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0)))
71	70	simprd 500	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (lastS‘𝑊) ≠ (𝑊‘0))
72		numclwwlk2lem1lem 30704	. . . . . . . . . 10 ⊢ ((𝑣 ∈ (Vtx‘𝐺) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0)) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0) ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ (𝑊‘0)))
73	68, 44, 71, 72	syl3anc 1397	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0) ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ (𝑊‘0)))
74		eqeq2 2774	. . . . . . . . . . . . 13 ⊢ (𝑋 = (𝑊‘0) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0)))
75	74	eqcoms 2770	. . . . . . . . . . . 12 ⊢ ((𝑊‘0) = 𝑋 → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0)))
76	75	ad2antrl 740	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0)))
77	76	ad2antlr 739	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0)))
78	73	simpld 499	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0))
79	78	neeq2d 3017	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0) ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ (𝑊‘0)))
80	77, 79	anbi12d 643	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)) ↔ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = (𝑊‘0) ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ (𝑊‘0))))
81	73, 80	mpbird 260	. . . . . . . 8 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)))
82		nncn 12247	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
83		2cnd 12325	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℂ)
84	82, 83	pncand 11576	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 2) − 2) = 𝑁)
85	84	3ad2ant3 1152	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑁 + 2) − 2) = 𝑁)
86	85	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑁 + 2) − 2) = 𝑁)
87	86	fveq2d 6885	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) = ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁))
88	87	neeq1d 3016	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0) ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)))
89	88	anbi2d 641	. . . . . . . 8 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)) ↔ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘𝑁) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0))))
90	81, 89	mpbird 260	. . . . . . 7 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)))
91	90	biantrud 540	. . . . . 6 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ ((𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)))))
92	61	anim2i 628	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ (ℤ_≥‘2)))
93	92	3adant1 1147	. . . . . . . . . 10 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ (ℤ_≥‘2)))
94	93	ad2antrr 738	. . . . . . . . 9 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ (ℤ_≥‘2)))
95		numclwwlk.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ_≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})
96	95	numclwwlkovh 30735	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ (ℤ_≥‘2)) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
97	94, 96	syl 18	. . . . . . . 8 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
98	97	eleq2d 2848	. . . . . . 7 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑊 ++ ⟨“𝑣”⟩) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}))
99		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 ++ ⟨“𝑣”⟩) → (𝑤‘0) = ((𝑊 ++ ⟨“𝑣”⟩)‘0))
100	99	eqeq1d 2764	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 ++ ⟨“𝑣”⟩) → ((𝑤‘0) = 𝑋 ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋))
101		fveq1 6880	. . . . . . . . . 10 ⊢ (𝑤 = (𝑊 ++ ⟨“𝑣”⟩) → (𝑤‘((𝑁 + 2) − 2)) = ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)))
102	101, 99	neeq12d 3018	. . . . . . . . 9 ⊢ (𝑤 = (𝑊 ++ ⟨“𝑣”⟩) → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0)))
103	100, 102	anbi12d 643	. . . . . . . 8 ⊢ (𝑤 = (𝑊 ++ ⟨“𝑣”⟩) → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0))))
104	103	elrab 3649	. . . . . . 7 ⊢ ((𝑊 ++ ⟨“𝑣”⟩) ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ ((𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0))))
105	98, 104	bitr2di 291	. . . . . 6 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑣”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ∧ (((𝑊 ++ ⟨“𝑣”⟩)‘0) = 𝑋 ∧ ((𝑊 ++ ⟨“𝑣”⟩)‘((𝑁 + 2) − 2)) ≠ ((𝑊 ++ ⟨“𝑣”⟩)‘0))) ↔ (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
106	67, 91, 105	3bitrd 308	. . . . 5 ⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) ∧ 𝑣 ∈ 𝑉) → (({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
107	106	reubidva 3382	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → (∃!𝑣 ∈ 𝑉 ({(lastS‘𝑊), 𝑣} ∈ (Edg‘𝐺) ∧ {𝑣, (𝑊‘0)} ∈ (Edg‘𝐺)) ↔ ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
108	42, 107	mpbid 235	. . 3 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ (𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋))) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)))
109	108	ex 417	. 2 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ ((𝑊‘0) = 𝑋 ∧ (lastS‘𝑊) ≠ 𝑋)) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
110	12, 109	sylbid 243	1 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃!wreu 3366 {crab 3415 Vcvv 3454 {cpr 4590 ‘cfv 6536 (class class class)co 7412 ∈ cmpo 7414 0cc0 11106 1c1 11107 + caddc 11109 − cmin 11447 ℕcn 12239 2c2 12301 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ..^cfzo 13689 ♯chash 14373 Word cword 14557 lastSclsw 14606 ++ cconcat 14614 ⟨“cs1 14640 Vtxcvtx 29357 Edgcedg 29408 WWalksN cwwlksn 30186 ClWWalksN cclwwlkn 30386 ClWWalksNOncclwwlknon 30449 FriendGraph cfrgr 30620

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-oadd 8455 df-er 8692 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-2 12309 df-n0 12511 df-xnn0 12584 df-z 12598 df-uz 12869 df-rp 13023 df-fz 13542 df-fzo 13690 df-hash 14374 df-word 14558 df-lsw 14607 df-concat 14615 df-s1 14641 df-wwlks 30190 df-wwlksn 30191 df-clwwlk 30344 df-clwwlkn 30387 df-clwwlknon 30450 df-frgr 30621

This theorem is used by: numclwlk2lem2f1o 30741

W3C validator