Metamath Proof Explorer

Theorem 0pthon

Description: A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 20-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0pthon.v 
|- V = ( Vtx ` G )
Assertion 0pthon 
|- ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( PathsOn ` G ) N ) P )

Proof

Step Hyp Ref Expression
1 0pthon.v 
 |-  V = ( Vtx ` G )
2 1 0trlon 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( TrailsOn ` G ) N ) P )
3 simpl 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P : ( 0 ... 0 ) --> V )
4 id 
 |-  ( P : ( 0 ... 0 ) --> V -> P : ( 0 ... 0 ) --> V )
5 0z 
 |-  0 e. ZZ
6 elfz3 
 |-  ( 0 e. ZZ -> 0 e. ( 0 ... 0 ) )
7 5 6 mp1i 
 |-  ( P : ( 0 ... 0 ) --> V -> 0 e. ( 0 ... 0 ) )
8 4 7 ffvelrnd 
 |-  ( P : ( 0 ... 0 ) --> V -> ( P ` 0 ) e. V )
9 8 adantr 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( P ` 0 ) e. V )
10 eleq1 
 |-  ( ( P ` 0 ) = N -> ( ( P ` 0 ) e. V <-> N e. V ) )
11 10 adantl 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( ( P ` 0 ) e. V <-> N e. V ) )
12 9 11 mpbid 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> N e. V )
13 1 1vgrex 
 |-  ( N e. V -> G e. _V )
14 1 0pth 
 |-  ( G e. _V -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
15 12 13 14 3syl 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( Paths ` G ) P <-> P : ( 0 ... 0 ) --> V ) )
16 3 15 mpbird 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( Paths ` G ) P )
17 1 0wlkonlem1 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( N e. V /\ N e. V ) )
18 1 0wlkonlem2 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> P e. ( V ^pm ( 0 ... 0 ) ) )
19 0ex 
 |-  (/) e. _V
20 18 19 jctil 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) e. _V /\ P e. ( V ^pm ( 0 ... 0 ) ) ) )
21 1 ispthson 
 |-  ( ( ( N e. V /\ N e. V ) /\ ( (/) e. _V /\ P e. ( V ^pm ( 0 ... 0 ) ) ) ) -> ( (/) ( N ( PathsOn ` G ) N ) P <-> ( (/) ( N ( TrailsOn ` G ) N ) P /\ (/) ( Paths ` G ) P ) ) )
22 17 20 21 syl2anc 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> ( (/) ( N ( PathsOn ` G ) N ) P <-> ( (/) ( N ( TrailsOn ` G ) N ) P /\ (/) ( Paths ` G ) P ) ) )
23 2 16 22 mpbir2and 
 |-  ( ( P : ( 0 ... 0 ) --> V /\ ( P ` 0 ) = N ) -> (/) ( N ( PathsOn ` G ) N ) P )