Theorem 0spth

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

	Ref	Expression
Hypothesis	0pth.v	|- V = ( Vtx ` G )
Assertion	0spth	|- ( G e. W -> ( (/) ( SPaths ` G ) P <-> P : ( 0 ... 0 ) --> V ) )

Proof

Step	Hyp	Ref	Expression
1		0pth.v	|- V = ( Vtx ` G )
2	1	0trl	|- ( G e. W -> ( (/) ( Trails ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
3	2	anbi1d	|- ( G e. W -> ( ( (/) ( Trails ` G ) P /\ Fun `' P ) <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' P ) ) )
4		isspth	|- ( (/) ( SPaths ` G ) P <-> ( (/) ( Trails ` G ) P /\ Fun `' P ) )
5		fz0sn	|- ( 0 ... 0 ) = { 0 }
6	5	feq2i	|- ( P : ( 0 ... 0 ) --> V <-> P : { 0 } --> V )
7		c0ex	|- 0 e. _V
8	7	fsn2	|- ( P : { 0 } --> V <-> ( ( P ` 0 ) e. V /\ P = { <. 0 , ( P ` 0 ) >. } ) )
9		funcnvsn	|- Fun `' { <. 0 , ( P ` 0 ) >. }
10		cnveq	|- ( P = { <. 0 , ( P ` 0 ) >. } -> `' P = `' { <. 0 , ( P ` 0 ) >. } )
11	10	funeqd	|- ( P = { <. 0 , ( P ` 0 ) >. } -> ( Fun `' P <-> Fun `' { <. 0 , ( P ` 0 ) >. } ) )
12	9 11	mpbiri	|- ( P = { <. 0 , ( P ` 0 ) >. } -> Fun `' P )
13	8 12	simplbiim	|- ( P : { 0 } --> V -> Fun `' P )
14	6 13	sylbi	|- ( P : ( 0 ... 0 ) --> V -> Fun `' P )
15	14	pm4.71i	|- ( P : ( 0 ... 0 ) --> V <-> ( P : ( 0 ... 0 ) --> V /\ Fun `' P ) )
16	3 4 15	3bitr4g	|- ( G e. W -> ( (/) ( SPaths ` G ) P <-> P : ( 0 ... 0 ) --> V ) )