Metamath Proof Explorer

Theorem conngrv2edg

Description: A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 . (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

Ref Expression
Hypotheses conngrv2edg.v 
|- V = ( Vtx ` G )
conngrv2edg.i 
|- I = ( iEdg ` G )
Assertion conngrv2edg 
|- ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> E. e e. ran I N e. e )

Proof

Step Hyp Ref Expression
1 conngrv2edg.v 
 |-  V = ( Vtx ` G )
2 conngrv2edg.i 
 |-  I = ( iEdg ` G )
3 1 fvexi 
 |-  V e. _V
4 simp3 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> 1 < ( # ` V ) )
5 simp2 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> N e. V )
6 hashgt12el2 
 |-  ( ( V e. _V /\ 1 < ( # ` V ) /\ N e. V ) -> E. v e. V N =/= v )
7 3 4 5 6 mp3an2i 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> E. v e. V N =/= v )
8 1 isconngr 
 |-  ( G e. ConnGraph -> ( G e. ConnGraph <-> A. a e. V A. b e. V E. f E. p f ( a ( PathsOn ` G ) b ) p ) )
9 oveq1 
 |-  ( a = N -> ( a ( PathsOn ` G ) b ) = ( N ( PathsOn ` G ) b ) )
10 9 breqd 
 |-  ( a = N -> ( f ( a ( PathsOn ` G ) b ) p <-> f ( N ( PathsOn ` G ) b ) p ) )
11 10 2exbidv 
 |-  ( a = N -> ( E. f E. p f ( a ( PathsOn ` G ) b ) p <-> E. f E. p f ( N ( PathsOn ` G ) b ) p ) )
12 oveq2 
 |-  ( b = v -> ( N ( PathsOn ` G ) b ) = ( N ( PathsOn ` G ) v ) )
13 12 breqd 
 |-  ( b = v -> ( f ( N ( PathsOn ` G ) b ) p <-> f ( N ( PathsOn ` G ) v ) p ) )
14 13 2exbidv 
 |-  ( b = v -> ( E. f E. p f ( N ( PathsOn ` G ) b ) p <-> E. f E. p f ( N ( PathsOn ` G ) v ) p ) )
15 11 14 rspc2v 
 |-  ( ( N e. V /\ v e. V ) -> ( A. a e. V A. b e. V E. f E. p f ( a ( PathsOn ` G ) b ) p -> E. f E. p f ( N ( PathsOn ` G ) v ) p ) )
16 15 ad2ant2r 
 |-  ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> ( A. a e. V A. b e. V E. f E. p f ( a ( PathsOn ` G ) b ) p -> E. f E. p f ( N ( PathsOn ` G ) v ) p ) )
17 pthontrlon 
 |-  ( f ( N ( PathsOn ` G ) v ) p -> f ( N ( TrailsOn ` G ) v ) p )
18 trlsonwlkon 
 |-  ( f ( N ( TrailsOn ` G ) v ) p -> f ( N ( WalksOn ` G ) v ) p )
19 simpl 
 |-  ( ( f ( N ( WalksOn ` G ) v ) p /\ ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) ) -> f ( N ( WalksOn ` G ) v ) p )
20 simprr 
 |-  ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> N =/= v )
21 wlkon2n0 
 |-  ( ( f ( N ( WalksOn ` G ) v ) p /\ N =/= v ) -> ( # ` f ) =/= 0 )
22 20 21 sylan2 
 |-  ( ( f ( N ( WalksOn ` G ) v ) p /\ ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) ) -> ( # ` f ) =/= 0 )
23 19 22 jca 
 |-  ( ( f ( N ( WalksOn ` G ) v ) p /\ ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) ) -> ( f ( N ( WalksOn ` G ) v ) p /\ ( # ` f ) =/= 0 ) )
24 23 ex 
 |-  ( f ( N ( WalksOn ` G ) v ) p -> ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> ( f ( N ( WalksOn ` G ) v ) p /\ ( # ` f ) =/= 0 ) ) )
25 17 18 24 3syl 
 |-  ( f ( N ( PathsOn ` G ) v ) p -> ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> ( f ( N ( WalksOn ` G ) v ) p /\ ( # ` f ) =/= 0 ) ) )
26 2 wlkonl1iedg 
 |-  ( ( f ( N ( WalksOn ` G ) v ) p /\ ( # ` f ) =/= 0 ) -> E. e e. ran I N e. e )
27 25 26 syl6com 
 |-  ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> ( f ( N ( PathsOn ` G ) v ) p -> E. e e. ran I N e. e ) )
28 27 exlimdvv 
 |-  ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> ( E. f E. p f ( N ( PathsOn ` G ) v ) p -> E. e e. ran I N e. e ) )
29 16 28 syldc 
 |-  ( A. a e. V A. b e. V E. f E. p f ( a ( PathsOn ` G ) b ) p -> ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> E. e e. ran I N e. e ) )
30 8 29 syl6bi 
 |-  ( G e. ConnGraph -> ( G e. ConnGraph -> ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> E. e e. ran I N e. e ) ) )
31 30 pm2.43i 
 |-  ( G e. ConnGraph -> ( ( ( N e. V /\ 1 < ( # ` V ) ) /\ ( v e. V /\ N =/= v ) ) -> E. e e. ran I N e. e ) )
32 31 expd 
 |-  ( G e. ConnGraph -> ( ( N e. V /\ 1 < ( # ` V ) ) -> ( ( v e. V /\ N =/= v ) -> E. e e. ran I N e. e ) ) )
33 32 3impib 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> ( ( v e. V /\ N =/= v ) -> E. e e. ran I N e. e ) )
34 33 expd 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> ( v e. V -> ( N =/= v -> E. e e. ran I N e. e ) ) )
35 34 rexlimdv 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> ( E. v e. V N =/= v -> E. e e. ran I N e. e ) )
36 7 35 mpd 
 |-  ( ( G e. ConnGraph /\ N e. V /\ 1 < ( # ` V ) ) -> E. e e. ran I N e. e )