Theorem 0ewlk

Description: The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021)

	Ref	Expression
Assertion	0ewlk	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ∅ ∈ ( 𝐺 EdgWalks 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		wrd0	⊢ ∅ ∈ Word dom ( iEdg ‘ 𝐺 )
2		ral0	⊢ ∀ 𝑘 ∈ ∅ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) )
3		hash0	⊢ ( ♯ ‘ ∅ ) = 0
4	3	oveq2i	⊢ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ( 1 ..^ 0 )
5		0le1	⊢ 0 ≤ 1
6		1z	⊢ 1 ∈ ℤ
7		0z	⊢ 0 ∈ ℤ
8		fzon	⊢ ( ( 1 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 0 ≤ 1 ↔ ( 1 ..^ 0 ) = ∅ ) )
9	6 7 8	mp2an	⊢ ( 0 ≤ 1 ↔ ( 1 ..^ 0 ) = ∅ )
10	5 9	mpbi	⊢ ( 1 ..^ 0 ) = ∅
11	4 10	eqtri	⊢ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅
12	11	raleqi	⊢ ( ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑘 ∈ ∅ 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) )
13	2 12	mpbir	⊢ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) )
14	1 13	pm3.2i	⊢ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) )
15		0ex	⊢ ∅ ∈ V
16		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
17	16	isewlk	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ ∅ ∈ V ) → ( ∅ ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ) ) )
18	15 17	mp3an3	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ( ∅ ∈ ( 𝐺 EdgWalks 𝑆 ) ↔ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 1 ..^ ( ♯ ‘ ∅ ) ) 𝑆 ≤ ( ♯ ‘ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ ( 𝑘 − 1 ) ) ) ∩ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ) ) )
19	14 18	mpbiri	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ) → ∅ ∈ ( 𝐺 EdgWalks 𝑆 ) )