Metamath Proof Explorer

Theorem 0wlk

Description: A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 3-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v ⊢ V = Vtx ⁡ G
Assertion 0wlk ⊢ G ∈ U → ∅ Walks ⁡ G P ↔ P : 0 … 0 ⟶ V

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 iswlkg ⊢ G ∈ U → ∅ Walks ⁡ G P ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ∧ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
4 ral0 ⊢ ∀ k ∈ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
5 hash0 ⊢ ∅ = 0
6 5 oveq2i ⊢ 0 ..^ ∅ = 0 ..^ 0
7 fzo0 ⊢ 0 ..^ 0 = ∅
8 6 7 eqtri ⊢ 0 ..^ ∅ = ∅
9 8 raleqi ⊢ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k ↔ ∀ k ∈ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
10 4 9 mpbir ⊢ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
11 10 biantru ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ∧ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
12 5 eqcomi ⊢ 0 = ∅
13 12 oveq2i ⊢ 0 … 0 = 0 … ∅
14 13 feq2i ⊢ P : 0 … 0 ⟶ V ↔ P : 0 … ∅ ⟶ V
15 wrd0 ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G
16 15 biantrur ⊢ P : 0 … ∅ ⟶ V ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V
17 14 16 bitri ⊢ P : 0 … 0 ⟶ V ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V
18 df-3an ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ∧ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k ↔ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ∧ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k
19 11 17 18 3bitr4ri ⊢ ∅ ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … ∅ ⟶ V ∧ ∀ k ∈ 0 ..^ ∅ if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ ∅ ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ ∅ ⁡ k ↔ P : 0 … 0 ⟶ V
20 3 19 syl6bb ⊢ G ∈ U → ∅ Walks ⁡ G P ↔ P : 0 … 0 ⟶ V