rusgrnumwwlkl1

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)

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

Proof

Step	Hyp	Ref	Expression
1		rusgrnumwwlkl1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		1nn0	⊢ 1 ∈ ℕ₀
3		iswwlksn	⊢ ( 1 ∈ ℕ₀ → ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ↔ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ) )
4	2 3	ax-mp	⊢ ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ↔ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) )
5		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6	1 5	iswwlks	⊢ ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
7	6	anbi1i	⊢ ( ( 𝑤 ∈ ( WWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) )
8	4 7	bitri	⊢ ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) )
9	8	a1i	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ) )
10	9	anbi1d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) )
11		1p1e2	⊢ ( 1 + 1 ) = 2
12	11	eqeq2i	⊢ ( ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = 2 )
13	12	a1i	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ↔ ( ♯ ‘ 𝑤 ) = 2 ) )
14	13	anbi2d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ↔ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ) )
15		3anass	⊢ ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
16	15	a1i	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
17		fveq2	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ ∅ ) )
18		hash0	⊢ ( ♯ ‘ ∅ ) = 0
19	17 18	eqtrdi	⊢ ( 𝑤 = ∅ → ( ♯ ‘ 𝑤 ) = 0 )
20		2ne0	⊢ 2 ≠ 0
21	20	nesymi	⊢ ¬ 0 = 2
22		eqeq1	⊢ ( ( ♯ ‘ 𝑤 ) = 0 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ 0 = 2 ) )
23	21 22	mtbiri	⊢ ( ( ♯ ‘ 𝑤 ) = 0 → ¬ ( ♯ ‘ 𝑤 ) = 2 )
24	19 23	syl	⊢ ( 𝑤 = ∅ → ¬ ( ♯ ‘ 𝑤 ) = 2 )
25	24	necon2ai	⊢ ( ( ♯ ‘ 𝑤 ) = 2 → 𝑤 ≠ ∅ )
26	25	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → 𝑤 ≠ ∅ )
27	26	biantrurd	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ≠ ∅ ∧ ( 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
28		oveq1	⊢ ( ( ♯ ‘ 𝑤 ) = 2 → ( ( ♯ ‘ 𝑤 ) − 1 ) = ( 2 − 1 ) )
29		2m1e1	⊢ ( 2 − 1 ) = 1
30	28 29	eqtrdi	⊢ ( ( ♯ ‘ 𝑤 ) = 2 → ( ( ♯ ‘ 𝑤 ) − 1 ) = 1 )
31	30	oveq2d	⊢ ( ( ♯ ‘ 𝑤 ) = 2 → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 0 ..^ 1 ) )
32	31	adantl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) = ( 0 ..^ 1 ) )
33	32	raleqdv	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 1 ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) )
34		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
35	34	raleqi	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 1 ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑖 ∈ { 0 } { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) )
36		c0ex	⊢ 0 ∈ V
37		fveq2	⊢ ( 𝑖 = 0 → ( 𝑤 ‘ 𝑖 ) = ( 𝑤 ‘ 0 ) )
38		fv0p1e1	⊢ ( 𝑖 = 0 → ( 𝑤 ‘ ( 𝑖 + 1 ) ) = ( 𝑤 ‘ 1 ) )
39	37 38	preq12d	⊢ ( 𝑖 = 0 → { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } )
40	39	eleq1d	⊢ ( 𝑖 = 0 → ( { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
41	36 40	ralsn	⊢ ( ∀ 𝑖 ∈ { 0 } { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
42	35 41	bitri	⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 1 ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) )
43	33 42	bitrdi	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ↔ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
44	43	anbi2d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ( 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
45	16 27 44	3bitr2d	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
46	45	ex	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑤 ) = 2 → ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
47	46	pm5.32rd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ↔ ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ) )
48	14 47	bitrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ↔ ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ) )
49	48	anbi1d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) )
50		anass	⊢ ( ( ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = 2 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) )
51	49 50	bitrdi	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( ( 𝑤 ≠ ∅ ∧ 𝑤 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑤 ) = ( 1 + 1 ) ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ) )
52		anass	⊢ ( ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ) )
53		ancom	⊢ ( ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
54		df-3an	⊢ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
55	53 54	bitr4i	⊢ ( ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ↔ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) )
56	55	anbi2i	⊢ ( ( 𝑤 ∈ Word 𝑉 ∧ ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
57	52 56	bitri	⊢ ( ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) )
58	57	a1i	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( ( 𝑤 ∈ Word 𝑉 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
59	10 51 58	3bitrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ( 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝑃 ) ↔ ( 𝑤 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
60	59	rabbidva2	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } )
61	60	fveq2d	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) )
62	1	rusgrnumwrdl2	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ ( Edg ‘ 𝐺 ) ) } ) = 𝐾 )
63	61 62	eqtrd	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉 ) → ( ♯ ‘ { 𝑤 ∈ ( 1 WWalksN 𝐺 ) ∣ ( 𝑤 ‘ 0 ) = 𝑃 } ) = 𝐾 )

Metamath Proof Explorer

Theorem rusgrnumwwlkl1

Proof