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