av-numclwlk2lem2f1o - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > av-numclwlk2lem2f1o		Structured version Visualization version GIF version

Theorem av-numclwlk2lem2f1o 41535

Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018.)

**Hypotheses**
Ref	Expression
av-numclwwlk.v	⊢ 𝑉 = (Vtx‘𝐺)
av-numclwwlk.q	⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)})
av-numclwwlk.f	⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣})
av-numclwwlk.h	⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))})
av-numclwwlk.r	⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 substr ⟨0, (𝑁 + 1)⟩))

**Assertion**
Ref	Expression
av-numclwlk2lem2f1o	⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁))

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

Proof of Theorem av-numclwlk2lem2f1o Dummy variables 𝑦 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2676	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))))
2		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑅‘𝑦) = (𝑅‘𝑥))
3		oveq1 6556	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (𝑦 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
4	2, 3	eqeq12d 2625	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((𝑅‘𝑦) = (𝑦 substr ⟨0, (𝑁 + 1)⟩) ↔ (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))
5	1, 4	imbi12d 333	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr ⟨0, (𝑁 + 1)⟩)) ↔ (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩))))
6	5	imbi2d 329	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr ⟨0, (𝑁 + 1)⟩))) ↔ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))))
7		av-numclwwlk.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
8		av-numclwwlk.q	. . . . . . . 8 ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ ( lastS ‘𝑤) ≠ 𝑣)})
9		av-numclwwlk.f	. . . . . . . 8 ⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ (𝑤‘0) = 𝑣})
10		av-numclwwlk.h	. . . . . . . 8 ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) ≠ (𝑤‘0))})
11		av-numclwwlk.r	. . . . . . . 8 ⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 substr ⟨0, (𝑁 + 1)⟩))
12	7, 8, 9, 10, 11	av-numclwlk2lem2fv 41534	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑦 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑦) = (𝑦 substr ⟨0, (𝑁 + 1)⟩)))
13	6, 12	chvarv 2251	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))
14	13	3adant1 1072	. . . . 5 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))
15	14	imp 444	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
16	7, 8, 9, 10, 11	av-numclwlk2lem2f 41533	. . . . 5 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁))
17	16	ffvelrnda 6267	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑅‘𝑥) ∈ (𝑋𝑄𝑁))
18	15, 17	eqeltrrd 2689	. . 3 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 substr ⟨0, (𝑁 + 1)⟩) ∈ (𝑋𝑄𝑁))
19	18	ralrimiva 2949	. 2 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 substr ⟨0, (𝑁 + 1)⟩) ∈ (𝑋𝑄𝑁))
20	7, 8, 9, 10	av-numclwwlk2lem1 41532	. . . . 5 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
21	20	imp 444	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)))
22	7, 8	av-numclwwlkovq 41529	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)})
23	22	eleq2d 2673	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}))
24	23	3adant1 1072	. . . . . . 7 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ 𝑢 ∈ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)}))
25		fveq1 6102	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0))
26	25	eqeq1d 2612	. . . . . . . . 9 ⊢ (𝑤 = 𝑢 → ((𝑤‘0) = 𝑋 ↔ (𝑢‘0) = 𝑋))
27		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → ( lastS ‘𝑤) = ( lastS ‘𝑢))
28	27	neeq1d 2841	. . . . . . . . 9 ⊢ (𝑤 = 𝑢 → (( lastS ‘𝑤) ≠ 𝑋 ↔ ( lastS ‘𝑢) ≠ 𝑋))
29	26, 28	anbi12d 743	. . . . . . . 8 ⊢ (𝑤 = 𝑢 → (((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋) ↔ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)))
30	29	elrab 3331	. . . . . . 7 ⊢ (𝑢 ∈ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ ( lastS ‘𝑤) ≠ 𝑋)} ↔ (𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)))
31	24, 30	syl6bb 275	. . . . . 6 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) ↔ (𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋))))
32		wwlknbp2 41063	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (𝑁 WWalkSN 𝐺) → (𝑢 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑢) = (𝑁 + 1)))
33	7	wrdeqi 13183	. . . . . . . . . . . . . . . . 17 ⊢ Word 𝑉 = Word (Vtx‘𝐺)
34	33	eleq2i 2680	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 ∈ Word 𝑉 ↔ 𝑢 ∈ Word (Vtx‘𝐺))
35	34	anbi1i 727	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ↔ (𝑢 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑢) = (𝑁 + 1)))
36	32, 35	sylibr 223	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (𝑁 WWalkSN 𝐺) → (𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)))
37		simpll 786	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → 𝑢 ∈ Word 𝑉)
38		id 22	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ)
39		2nn 11062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℕ
40	39	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℕ)
41	38, 40	nnaddcld 10944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ ℕ → (𝑁 + 2) ∈ ℕ)
42	7, 8, 9, 10	av-numclwwlkovh 41531	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑋 ∈ 𝑉 ∧ (𝑁 + 2) ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
43	41, 42	sylan2 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝐻(𝑁 + 2)) = {𝑤 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))})
44	43	eleq2d 2673	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ 𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))}))
45		fveq1 6102	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑤‘0) = (𝑥‘0))
46	45	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑤‘0) = 𝑋 ↔ (𝑥‘0) = 𝑋))
47		fveq1 6102	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = 𝑥 → (𝑤‘((𝑁 + 2) − 2)) = (𝑥‘((𝑁 + 2) − 2)))
48	47, 45	neeq12d 2843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑥 → ((𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0) ↔ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))
49	46, 48	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑥 → (((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0)) ↔ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))
50	49	elrab 3331	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ {𝑤 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘((𝑁 + 2) − 2)) ≠ (𝑤‘0))} ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))))
51	44, 50	syl6bb 275	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
52	51	3adant1 1072	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
53	52	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↔ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0)))))
54	7	clwwlknbp 41193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 2)))
55		lencl 13179	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑢 ∈ Word 𝑉 → (#‘𝑢) ∈ ℕ₀)
56		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → 𝑥 ∈ Word 𝑉)
57		df-2 10956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ 2 = (1 + 1)
58	57	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 2 = (1 + 1))
59	58	oveq2d 6565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = (𝑁 + (1 + 1)))
60		nncn 10905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
61		1cnd 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
62	60, 61, 61	addassd 9941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
63	59, 62	eqtr4d 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → (𝑁 + 2) = ((𝑁 + 1) + 1))
64	63	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (𝑁 + 2) = ((𝑁 + 1) + 1))
65	64	eqeq2d 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → ((#‘𝑥) = (𝑁 + 2) ↔ (#‘𝑥) = ((𝑁 + 1) + 1)))
66	65	biimpcd 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((#‘𝑥) = (𝑁 + 2) → ((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘𝑥) = ((𝑁 + 1) + 1)))
67	66	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → ((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) → (#‘𝑥) = ((𝑁 + 1) + 1)))
68	67	impcom 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (#‘𝑥) = ((𝑁 + 1) + 1))
69		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((#‘𝑢) = (𝑁 + 1) → ((#‘𝑢) + 1) = ((𝑁 + 1) + 1))
70	69	ad3antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → ((#‘𝑢) + 1) = ((𝑁 + 1) + 1))
71	68, 70	eqtr4d 2647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (#‘𝑥) = ((#‘𝑢) + 1))
72	56, 71	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) ∧ 𝑁 ∈ ℕ) ∧ ((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))
73	72	exp31 628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((#‘𝑢) ∈ ℕ₀ ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
74	55, 73	sylan 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 ∈ ℕ → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
75	74	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
76	75	3ad2ant3 1077	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
77	76	impcom 445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
78	77	com12 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((#‘𝑥) = (𝑁 + 2) ∧ 𝑥 ∈ Word 𝑉) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
79	78	ancoms 468	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = (𝑁 + 2)) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
80	54, 79	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
81	80	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
82	81	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ((𝑥 ∈ ((𝑁 + 2) ClWWalkSN 𝐺) ∧ ((𝑥‘0) = 𝑋 ∧ (𝑥‘((𝑁 + 2) − 2)) ≠ (𝑥‘0))) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
83	53, 82	sylbid 229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
84	83	ralrimiv 2948	. . . . . . . . . . . . . . . 16 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))
85	37, 84	jca 553	. . . . . . . . . . . . . . 15 ⊢ (((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
86	85	ex 449	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
87	36, 86	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (𝑁 WWalkSN 𝐺) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
88	87	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1)))))
89	88	imp 444	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))))
90		reuccats1 13332	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ Word 𝑉 ∧ ∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 ∈ Word 𝑉 ∧ (#‘𝑥) = ((#‘𝑢) + 1))) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (#‘𝑢)⟩)))
91	89, 90	syl 17	. . . . . . . . . 10 ⊢ (((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (#‘𝑢)⟩)))
92	91	imp 444	. . . . . . . . 9 ⊢ ((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (#‘𝑢)⟩))
93		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (#‘𝑢) = (𝑁 + 1))
94	93	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ Word 𝑉 ∧ (#‘𝑢) = (𝑁 + 1)) → (𝑁 + 1) = (#‘𝑢))
95	36, 94	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (𝑁 WWalkSN 𝐺) → (𝑁 + 1) = (#‘𝑢))
96	95	ad4antr 764	. . . . . . . . . . . . 13 ⊢ (((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑁 + 1) = (#‘𝑢))
97	96	opeq2d 4347	. . . . . . . . . . . 12 ⊢ (((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → ⟨0, (𝑁 + 1)⟩ = ⟨0, (#‘𝑢)⟩)
98	97	oveq2d 6565	. . . . . . . . . . 11 ⊢ (((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑥 substr ⟨0, (𝑁 + 1)⟩) = (𝑥 substr ⟨0, (#‘𝑢)⟩))
99	98	eqeq2d 2620	. . . . . . . . . 10 ⊢ (((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) ∧ 𝑥 ∈ (𝑋𝐻(𝑁 + 2))) → (𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩) ↔ 𝑢 = (𝑥 substr ⟨0, (#‘𝑢)⟩)))
100	99	reubidva 3102	. . . . . . . . 9 ⊢ ((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → (∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩) ↔ ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (#‘𝑢)⟩)))
101	92, 100	mpbird 246	. . . . . . . 8 ⊢ ((((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) ∧ (𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) ∧ ∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
102	101	exp31 628	. . . . . . 7 ⊢ ((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))))
103	102	com12 32	. . . . . 6 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑢 ∈ (𝑁 WWalkSN 𝐺) ∧ ((𝑢‘0) = 𝑋 ∧ ( lastS ‘𝑢) ≠ 𝑋)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))))
104	31, 103	sylbid 229	. . . . 5 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑢 ∈ (𝑋𝑄𝑁) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))))
105	104	imp 444	. . . 4 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → (∃!𝑣 ∈ 𝑉 (𝑢 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))
106	21, 105	mpd 15	. . 3 ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) ∧ 𝑢 ∈ (𝑋𝑄𝑁)) → ∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
107	106	ralrimiva 2949	. 2 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩))
108	11	f1ompt 6290	. 2 ⊢ (𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁) ↔ (∀𝑥 ∈ (𝑋𝐻(𝑁 + 2))(𝑥 substr ⟨0, (𝑁 + 1)⟩) ∈ (𝑋𝑄𝑁) ∧ ∀𝑢 ∈ (𝑋𝑄𝑁)∃!𝑥 ∈ (𝑋𝐻(𝑁 + 2))𝑢 = (𝑥 substr ⟨0, (𝑁 + 1)⟩)))
109	19, 107, 108	sylanbrc 695	1 ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ≠ wne 2780 ∀wral 2896 ∃!wreu 2898 {crab 2900 ⟨cop 4131 ↦ cmpt 4643 –1-1-onto→wf1o 5803 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 0cc0 9815 1c1 9816 + caddc 9818 − cmin 10145 ℕcn 10897 2c2 10947 ℕ₀cn0 11169 #chash 12979 Word cword 13146 lastS clsw 13147 ++ cconcat 13148 ⟨“cs1 13149 substr csubstr 13150 Vtxcvtx 25673 WWalkSN cwwlksn 41029 ClWWalkSN cclwwlksn 41184 FriendGraph cfrgr 41428

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-xnn0 11241 df-z 11255 df-uz 11564 df-rp 11709 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-lsw 13155 df-concat 13156 df-s1 13157 df-substr 13158 df-wwlks 41033 df-wwlksn 41034 df-clwwlks 41185 df-clwwlksn 41186 df-frgr 41429

This theorem is referenced by: av-numclwwlk2lem3 41536

W3C validator