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 \in ConnGraph \land N \in V \land 1 < \|V\|) \to \exists e \in ran I N \in e$

Proof

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

Metamath Proof Explorer

Theorem conngrv2edg

Proof