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 ConnGraph N V 1 < V e ran I N e

Proof

Step Hyp Ref Expression
1 conngrv2edg.v V = Vtx G
2 conngrv2edg.i I = iEdg G
3 1 fvexi V V
4 simp3 G ConnGraph N V 1 < V 1 < V
5 simp2 G ConnGraph N V 1 < V N V
6 hashgt12el2 V V 1 < V N V v V N v
7 3 4 5 6 mp3an2i G ConnGraph N V 1 < V v V N v
8 1 isconngr G ConnGraph G ConnGraph a V b V f 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 f p f a PathsOn G b p f 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 f p f N PathsOn G b p f p f N PathsOn G v p
15 11 14 rspc2v N V v V a V b V f p f a PathsOn G b p f p f N PathsOn G v p
16 15 ad2ant2r N V 1 < V v V N v a V b V f p f a PathsOn G b p f 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 V 1 < V v V N v f N WalksOn G v p
20 simprr N V 1 < V v 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 V 1 < V v V N v f 0
23 19 22 jca f N WalksOn G v p N V 1 < V v V N v f N WalksOn G v p f 0
24 23 ex f N WalksOn G v p N V 1 < V v V N v f N WalksOn G v p f 0
25 17 18 24 3syl f N PathsOn G v p N V 1 < V v V N v f N WalksOn G v p f 0
26 2 wlkonl1iedg f N WalksOn G v p f 0 e ran I N e
27 25 26 syl6com N V 1 < V v V N v f N PathsOn G v p e ran I N e
28 27 exlimdvv N V 1 < V v V N v f p f N PathsOn G v p e ran I N e
29 16 28 syldc a V b V f p f a PathsOn G b p N V 1 < V v V N v e ran I N e
30 8 29 syl6bi G ConnGraph G ConnGraph N V 1 < V v V N v e ran I N e
31 30 pm2.43i G ConnGraph N V 1 < V v V N v e ran I N e
32 31 expd G ConnGraph N V 1 < V v V N v e ran I N e
33 32 3impib G ConnGraph N V 1 < V v V N v e ran I N e
34 33 expd G ConnGraph N V 1 < V v V N v e ran I N e
35 34 rexlimdv G ConnGraph N V 1 < V v V N v e ran I N e
36 7 35 mpd G ConnGraph N V 1 < V e ran I N e