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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0wlk ( 𝐺 ∈ 𝑈 → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 iswlkg ⊢ ( 𝐺 ∈ 𝑈 → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ) )
4 ral0 ⊢ ∀ 𝑘 ∈ ∅ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) )
5 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
6 5 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ( 0 ..^ 0 )
7 fzo0 ⊢ ( 0 ..^ 0 ) = ∅
8 6 7 eqtri ⊢ ( 0 ..^ ( ♯ ‘ ∅ ) ) = ∅
9 8 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ↔ ∀ 𝑘 ∈ ∅ if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) )
10 4 9 mpbir ⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) )
11 10 biantru ⊢ ( ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ) ↔ ( ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) )
12 5 eqcomi ⊢ 0 = ( ♯ ‘ ∅ )
13 12 oveq2i ⊢ ( 0 ... 0 ) = ( 0 ... ( ♯ ‘ ∅ ) )
14 13 feq2i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 )
15 wrd0 ⊢ ∅ ∈ Word dom ( iEdg ‘ 𝐺 )
16 15 biantrur ⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ↔ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ) )
17 14 16 bitri ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ) )
18 df-3an ⊢ ( ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ↔ ( ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) )
19 11 17 18 3bitr4ri ⊢ ( ( ∅ ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ ∅ ) ) ⟶ 𝑉 ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ ∅ ) ) if- ( ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) } , { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ∅ ‘ 𝑘 ) ) ) ) ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
20 3 19 bitrdi ⊢ ( 𝐺 ∈ 𝑈 → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )