Metamath Proof Explorer

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 ⊢ G ∈ V ∧ S ∈ ℕ 0 * → ∅ ∈ G EdgWalks S

Proof

Step Hyp Ref Expression
1 wrd0 ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G
2 ral0 ⊢ ∀ k ∈ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
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 ⊢ ∀ k ∈ 1 ..^ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k ↔ ∀ k ∈ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
13 2 12 mpbir ⊢ ∀ k ∈ 1 ..^ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
14 1 13 pm3.2i ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 1 ..^ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
15 0ex ⊢ ∅ ∈ V
16 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
17 16 isewlk ⊢ G ∈ V ∧ S ∈ ℕ 0 * ∧ ∅ ∈ V → ∅ ∈ G EdgWalks S ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 1 ..^ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
18 15 17 mp3an3 ⊢ G ∈ V ∧ S ∈ ℕ 0 * → ∅ ∈ G EdgWalks S ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 1 ..^ ∅ S ≤ iEdg ⁡ G ⁡ ∅ ⁡ k − 1 ∩ iEdg ⁡ G ⁡ ∅ ⁡ k
19 14 18 mpbiri ⊢ G ∈ V ∧ S ∈ ℕ 0 * → ∅ ∈ G EdgWalks S