This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )