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⁡GP↔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⁡GP↔∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V∧∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k
4 ral0 ⊢∀k∈∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡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+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k↔∀k∈∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k
10 4 9 mpbir ⊢∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k
11 10 biantru ⊢∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V↔∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V∧∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡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 ⊢∅∈Worddom⁡iEdg⁡G
16 15 biantrur ⊢P:0…∅⟶V↔∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V
17 14 16 bitri ⊢P:0…0⟶V↔∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V
18 df-3an ⊢∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V∧∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k↔∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V∧∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k
19 11 17 18 3bitr4ri ⊢∅∈Worddom⁡iEdg⁡G∧P:0…∅⟶V∧∀k∈0..^∅if-P⁡k=P⁡k+1iEdg⁡G⁡∅⁡k=P⁡kP⁡kP⁡k+1⊆iEdg⁡G⁡∅⁡k↔P:0…0⟶V
20 3 19 bitrdi ⊢G∈U→∅Walks⁡GP↔P:0…0⟶V