Metamath Proof Explorer

Theorem wlkonl1iedg

Description: If there is a walk between two vertices A and B at least of length 1, then the start vertex A is incident with an edge. (Contributed by AV, 4-Apr-2021)

Ref Expression
Hypothesis wlkonl1iedg.i 
|- I = ( iEdg ` G )
Assertion wlkonl1iedg 
|- ( ( F ( A ( WalksOn ` G ) B ) P /\ ( # ` F ) =/= 0 ) -> E. e e. ran I A e. e )

Proof

Step Hyp Ref Expression
1 wlkonl1iedg.i 
 |-  I = ( iEdg ` G )
2 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
3 2 wlkonprop 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
4 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
5 fv0p1e1 
 |-  ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
6 4 5 preq12d 
 |-  ( k = 0 -> { ( P ` k ) , ( P ` ( k + 1 ) ) } = { ( P ` 0 ) , ( P ` 1 ) } )
7 6 sseq1d 
 |-  ( k = 0 -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> { ( P ` 0 ) , ( P ` 1 ) } C_ e ) )
8 7 rexbidv 
 |-  ( k = 0 -> ( E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e <-> E. e e. ran I { ( P ` 0 ) , ( P ` 1 ) } C_ e ) )
9 1 wlkvtxiedg 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
10 9 adantr 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
11 10 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) /\ ( # ` F ) =/= 0 ) -> A. k e. ( 0 ..^ ( # ` F ) ) E. e e. ran I { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ e )
12 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
13 elnnne0 
 |-  ( ( # ` F ) e. NN <-> ( ( # ` F ) e. NN0 /\ ( # ` F ) =/= 0 ) )
14 13 simplbi2 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) =/= 0 -> ( # ` F ) e. NN ) )
15 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
16 14 15 imbitrrdi 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) =/= 0 -> 0 e. ( 0 ..^ ( # ` F ) ) ) )
17 12 16 syl 
 |-  ( F ( Walks ` G ) P -> ( ( # ` F ) =/= 0 -> 0 e. ( 0 ..^ ( # ` F ) ) ) )
18 17 adantr 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( ( # ` F ) =/= 0 -> 0 e. ( 0 ..^ ( # ` F ) ) ) )
19 18 imp 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) /\ ( # ` F ) =/= 0 ) -> 0 e. ( 0 ..^ ( # ` F ) ) )
20 8 11 19 rspcdva 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) /\ ( # ` F ) =/= 0 ) -> E. e e. ran I { ( P ` 0 ) , ( P ` 1 ) } C_ e )
21 fvex 
 |-  ( P ` 0 ) e. _V
22 fvex 
 |-  ( P ` 1 ) e. _V
23 21 22 prss 
 |-  ( ( ( P ` 0 ) e. e /\ ( P ` 1 ) e. e ) <-> { ( P ` 0 ) , ( P ` 1 ) } C_ e )
24 eleq1 
 |-  ( ( P ` 0 ) = A -> ( ( P ` 0 ) e. e <-> A e. e ) )
25 ax-1 
 |-  ( A e. e -> ( ( P ` 1 ) e. e -> A e. e ) )
26 24 25 biimtrdi 
 |-  ( ( P ` 0 ) = A -> ( ( P ` 0 ) e. e -> ( ( P ` 1 ) e. e -> A e. e ) ) )
27 26 adantl 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( ( P ` 0 ) e. e -> ( ( P ` 1 ) e. e -> A e. e ) ) )
28 27 impd 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( ( ( P ` 0 ) e. e /\ ( P ` 1 ) e. e ) -> A e. e ) )
29 23 28 biimtrrid 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ e -> A e. e ) )
30 29 reximdv 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( E. e e. ran I { ( P ` 0 ) , ( P ` 1 ) } C_ e -> E. e e. ran I A e. e ) )
31 30 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) /\ ( # ` F ) =/= 0 ) -> ( E. e e. ran I { ( P ` 0 ) , ( P ` 1 ) } C_ e -> E. e e. ran I A e. e ) )
32 20 31 mpd 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) /\ ( # ` F ) =/= 0 ) -> E. e e. ran I A e. e )
33 32 ex 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A ) -> ( ( # ` F ) =/= 0 -> E. e e. ran I A e. e ) )
34 33 3adant3 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` F ) =/= 0 -> E. e e. ran I A e. e ) )
35 34 3ad2ant3 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( ( # ` F ) =/= 0 -> E. e e. ran I A e. e ) )
36 3 35 syl 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( # ` F ) =/= 0 -> E. e e. ran I A e. e ) )
37 36 imp 
 |-  ( ( F ( A ( WalksOn ` G ) B ) P /\ ( # ` F ) =/= 0 ) -> E. e e. ran I A e. e )