Theorem 0trl

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

	Ref	Expression
Hypothesis	0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	0trl	$$⊢G\in U\to \left(\varnothing \mathrm{Trails}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	0wlk	$$⊢G\in U\to \left(\varnothing \mathrm{Walks}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$
3	2	anbi1d	$$⊢G\in U\to \left(\left(\varnothing \mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{\varnothing }^{-1}\right)\leftrightarrow \left(P:\left(0\dots 0\right)⟶V\wedge \mathrm{Fun}{\varnothing }^{-1}\right)\right)$$
4		istrl	$$⊢\varnothing \mathrm{Trails}\left(G\right)P\leftrightarrow \left(\varnothing \mathrm{Walks}\left(G\right)P\wedge \mathrm{Fun}{\varnothing }^{-1}\right)$$
5		funcnv0	$$⊢\mathrm{Fun}{\varnothing }^{-1}$$
6	5	biantru	$$⊢P:\left(0\dots 0\right)⟶V\leftrightarrow \left(P:\left(0\dots 0\right)⟶V\wedge \mathrm{Fun}{\varnothing }^{-1}\right)$$
7	3 4 6	3bitr4g	$$⊢G\in U\to \left(\varnothing \mathrm{Trails}\left(G\right)P\leftrightarrow P:\left(0\dots 0\right)⟶V\right)$$