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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	conngrv2edg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion	conngrv2edg	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 )

Proof

Step	Hyp	Ref	Expression
1		conngrv2edg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		conngrv2edg.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3	1	fvexi	⊢ 𝑉 ∈ V
4		simp3	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → 1 < ( ♯ ‘ 𝑉 ) )
5		simp2	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → 𝑁 ∈ 𝑉 )
6		hashgt12el2	⊢ ( ( 𝑉 ∈ V ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝑁 ∈ 𝑉 ) → ∃ 𝑣 ∈ 𝑉 𝑁 ≠ 𝑣 )
7	3 4 5 6	mp3an2i	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑣 ∈ 𝑉 𝑁 ≠ 𝑣 )
8	1	isconngr	⊢ ( 𝐺 ∈ ConnGraph → ( 𝐺 ∈ ConnGraph ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ) )
9		oveq1	⊢ ( 𝑎 = 𝑁 → ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) = ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) )
10	9	breqd	⊢ ( 𝑎 = 𝑁 → ( 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ↔ 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ) )
11	10	2exbidv	⊢ ( 𝑎 = 𝑁 → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ) )
12		oveq2	⊢ ( 𝑏 = 𝑣 → ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) = ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) )
13	12	breqd	⊢ ( 𝑏 = 𝑣 → ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ↔ 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 ) )
14	13	2exbidv	⊢ ( 𝑏 = 𝑣 → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ↔ ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 ) )
15	11 14	rspc2v	⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 ) )
16	15	ad2ant2r	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 → ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 ) )
17		pthontrlon	⊢ ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 → 𝑓 ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑣 ) 𝑝 )
18		trlsonwlkon	⊢ ( 𝑓 ( 𝑁 ( TrailsOn ‘ 𝐺 ) 𝑣 ) 𝑝 → 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 )
19		simpl	⊢ ( ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) ) → 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 )
20		simprr	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → 𝑁 ≠ 𝑣 )
21		wlkon2n0	⊢ ( ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ 𝑁 ≠ 𝑣 ) → ( ♯ ‘ 𝑓 ) ≠ 0 )
22	20 21	sylan2	⊢ ( ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) ) → ( ♯ ‘ 𝑓 ) ≠ 0 )
23	19 22	jca	⊢ ( ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) ) → ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) ≠ 0 ) )
24	23	ex	⊢ ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 → ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) ≠ 0 ) ) )
25	17 18 24	3syl	⊢ ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 → ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) ≠ 0 ) ) )
26	2	wlkonl1iedg	⊢ ( ( 𝑓 ( 𝑁 ( WalksOn ‘ 𝐺 ) 𝑣 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) ≠ 0 ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 )
27	25 26	syl6com	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ( 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
28	27	exlimdvv	⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ( ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑁 ( PathsOn ‘ 𝐺 ) 𝑣 ) 𝑝 → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
29	16 28	syldc	⊢ ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑓 ∃ 𝑝 𝑓 ( 𝑎 ( PathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 → ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
30	8 29	biimtrdi	⊢ ( 𝐺 ∈ ConnGraph → ( 𝐺 ∈ ConnGraph → ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) ) )
31	30	pm2.43i	⊢ ( 𝐺 ∈ ConnGraph → ( ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
32	31	expd	⊢ ( 𝐺 ∈ ConnGraph → ( ( 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) ) )
33	32	3impib	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ 𝑁 ≠ 𝑣 ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
34	33	expd	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑣 ∈ 𝑉 → ( 𝑁 ≠ 𝑣 → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) ) )
35	34	rexlimdv	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∃ 𝑣 ∈ 𝑉 𝑁 ≠ 𝑣 → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 ) )
36	7 35	mpd	⊢ ( ( 𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒 )