rusgrnumwwlkl1 - Metamath Proof Explorer

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

Theorem rusgrnumwwlkl1 27749

Description: In a k-regular graph, there are k walks (as word) of length 1 starting at each vertex. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 7-May-2021.)

**Hypothesis**
Ref	Expression
rusgrnumwwlkl1.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
rusgrnumwwlkl1	⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = 𝐾)

Distinct variable groups: 𝑤,𝐺 𝑤,𝐾 𝑤,𝑃 𝑤,𝑉

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

Step	Hyp	Ref	Expression
1		1nn0 11916	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
2		iswwlksn 27618	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑤 ∈ (1 WWalksN 𝐺) ↔ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (1 + 1))))
3	1, 2	ax-mp 5	. . . . . . . 8 ⊢ (𝑤 ∈ (1 WWalksN 𝐺) ↔ (𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (1 + 1)))
4		rusgrnumwwlkl1.v	. . . . . . . . . 10 ⊢ 𝑉 = (Vtx‘𝐺)
5		eqid 2823	. . . . . . . . . 10 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
6	4, 5	iswwlks 27616	. . . . . . . . 9 ⊢ (𝑤 ∈ (WWalks‘𝐺) ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
7	6	anbi1i 625	. . . . . . . 8 ⊢ ((𝑤 ∈ (WWalks‘𝐺) ∧ (♯‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)))
8	3, 7	bitri 277	. . . . . . 7 ⊢ (𝑤 ∈ (1 WWalksN 𝐺) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)))
9	8	a1i 11	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (𝑤 ∈ (1 WWalksN 𝐺) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1))))
10	9	anbi1d 631	. . . . 5 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ (1 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃)))
11		1p1e2 11765	. . . . . . . . . . 11 ⊢ (1 + 1) = 2
12	11	eqeq2i 2836	. . . . . . . . . 10 ⊢ ((♯‘𝑤) = (1 + 1) ↔ (♯‘𝑤) = 2)
13	12	a1i 11	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((♯‘𝑤) = (1 + 1) ↔ (♯‘𝑤) = 2))
14	13	anbi2d 630	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)) ↔ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2)))
15		3anass 1091	. . . . . . . . . . . 12 ⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))))
16	15	a1i 11	. . . . . . . . . . 11 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
17		fveq2 6672	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ∅ → (♯‘𝑤) = (♯‘∅))
18		hash0 13731	. . . . . . . . . . . . . . . 16 ⊢ (♯‘∅) = 0
19	17, 18	syl6eq 2874	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ∅ → (♯‘𝑤) = 0)
20		2ne0 11744	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
21	20	nesymi 3075	. . . . . . . . . . . . . . . 16 ⊢ ¬ 0 = 2
22		eqeq1 2827	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑤) = 0 → ((♯‘𝑤) = 2 ↔ 0 = 2))
23	21, 22	mtbiri 329	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑤) = 0 → ¬ (♯‘𝑤) = 2)
24	19, 23	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ∅ → ¬ (♯‘𝑤) = 2)
25	24	necon2ai 3047	. . . . . . . . . . . . 13 ⊢ ((♯‘𝑤) = 2 → 𝑤 ≠ ∅)
26	25	adantl 484	. . . . . . . . . . . 12 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → 𝑤 ≠ ∅)
27	26	biantrurd 535	. . . . . . . . . . 11 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ≠ ∅ ∧ (𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))))
28		oveq1 7165	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑤) = 2 → ((♯‘𝑤) − 1) = (2 − 1))
29		2m1e1 11766	. . . . . . . . . . . . . . . . 17 ⊢ (2 − 1) = 1
30	28, 29	syl6eq 2874	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑤) = 2 → ((♯‘𝑤) − 1) = 1)
31	30	oveq2d 7174	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝑤) = 2 → (0..^((♯‘𝑤) − 1)) = (0..^1))
32	31	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → (0..^((♯‘𝑤) − 1)) = (0..^1))
33	32	raleqdv 3417	. . . . . . . . . . . . 13 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → (∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)))
34		fzo01 13122	. . . . . . . . . . . . . . 15 ⊢ (0..^1) = {0}
35	34	raleqi 3415	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ (0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ {0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺))
36		c0ex 10637	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
37		fveq2 6672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 0 → (𝑤‘𝑖) = (𝑤‘0))
38		fv0p1e1 11763	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 0 → (𝑤‘(𝑖 + 1)) = (𝑤‘1))
39	37, 38	preq12d 4679	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 0 → {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} = {(𝑤‘0), (𝑤‘1)})
40	39	eleq1d 2899	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 0 → ({(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))
41	36, 40	ralsn 4621	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ {0} {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))
42	35, 41	bitri 277	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (0..^1){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))
43	33, 42	syl6bb 289	. . . . . . . . . . . 12 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → (∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))
44	43	anbi2d 630	. . . . . . . . . . 11 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → ((𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))
45	16, 27, 44	3bitr2d 309	. . . . . . . . . 10 ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) ∧ (♯‘𝑤) = 2) → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))
46	45	ex 415	. . . . . . . . 9 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((♯‘𝑤) = 2 → ((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ↔ (𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))))
47	46	pm5.32rd 580	. . . . . . . 8 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2)))
48	14, 47	bitrd 281	. . . . . . 7 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2)))
49	48	anbi1d 631	. . . . . 6 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃)))
50		anass 471	. . . . . 6 ⊢ ((((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = 2) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)))
51	49, 50	syl6bb 289	. . . . 5 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((((𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑤) = (1 + 1)) ∧ (𝑤‘0) = 𝑃) ↔ ((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))))
52		anass 471	. . . . . . 7 ⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))))
53		ancom 463	. . . . . . . . 9 ⊢ (({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))
54		df-3an 1085	. . . . . . . . 9 ⊢ (((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ↔ (((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃) ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))
55	53, 54	bitr4i 280	. . . . . . . 8 ⊢ (({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))
56	55	anbi2i 624	. . . . . . 7 ⊢ ((𝑤 ∈ Word 𝑉 ∧ ({(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃))) ↔ (𝑤 ∈ Word 𝑉 ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))
57	52, 56	bitri 277	. . . . . 6 ⊢ (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))))
58	57	a1i 11	. . . . 5 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (((𝑤 ∈ Word 𝑉 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)) ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃)) ↔ (𝑤 ∈ Word 𝑉 ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))))
59	10, 51, 58	3bitrd 307	. . . 4 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → ((𝑤 ∈ (1 WWalksN 𝐺) ∧ (𝑤‘0) = 𝑃) ↔ (𝑤 ∈ Word 𝑉 ∧ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺)))))
60	59	rabbidva2 3478	. . 3 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → {𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃} = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))})
61	60	fveq2d 6676	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = (♯‘{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}))
62	4	rusgrnumwrdl2 27370	. 2 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾)
63	61, 62	eqtrd 2858	1 ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ (1 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}) = 𝐾)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∀wral 3140 {crab 3144 ∅c0 4293 {csn 4569 {cpr 4571 class class class wbr 5068 ‘cfv 6357 (class class class)co 7158 0cc0 10539 1c1 10540 + caddc 10542 − cmin 10872 2c2 11695 ℕ₀cn0 11900 ..^cfzo 13036 ♯chash 13693 Word cword 13864 Vtxcvtx 26783 Edgcedg 26834 RegUSGraph crusgr 27340 WWalkscwwlks 27605 WWalksN cwwlksn 27606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-rep 5192 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-int 4879 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-1st 7691 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-1o 8104 df-2o 8105 df-oadd 8108 df-er 8291 df-map 8410 df-en 8512 df-dom 8513 df-sdom 8514 df-fin 8515 df-dju 9332 df-card 9370 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-nn 11641 df-2 11703 df-n0 11901 df-xnn0 11971 df-z 11985 df-uz 12247 df-xadd 12511 df-fz 12896 df-fzo 13037 df-hash 13694 df-word 13865 df-edg 26835 df-uhgr 26845 df-ushgr 26846 df-upgr 26869 df-umgr 26870 df-uspgr 26937 df-usgr 26938 df-nbgr 27117 df-vtxdg 27250 df-rgr 27341 df-rusgr 27342 df-wwlks 27610 df-wwlksn 27611

This theorem is referenced by: rusgrnumwwlkb1 27753

W3C validator