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 bitrdi G U Walks G P P : 0 0 V