vdn0conngrumgrv2

Description: A vertex in a connected multigraph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017) (Revised by AV, 4-Apr-2021)

		Ref	Expression
	Hypothesis	vdn0conngrv2.v	$⊢ V = Vtx (G)$
	Assertion	vdn0conngrumgrv2	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to VtxDeg (G) (N) \neq 0$

Proof

Step	Hyp	Ref	Expression
1		vdn0conngrv2.v	$⊢ V = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3		eqid	$⊢ dom iEdg (G) = dom iEdg (G)$
4		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
5	1 2 3 4	vtxdumgrval	$⊢ (G \in UMGraph \land N \in V) \to VtxDeg (G) (N) = \|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\|$
6	5	ad2ant2lr	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to VtxDeg (G) (N) = \|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\|$
7		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
8	2	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
9		funfn	$⊢ Fun iEdg (G) \leftrightarrow iEdg (G) Fn dom iEdg (G)$
10	9	biimpi	$⊢ Fun iEdg (G) \to iEdg (G) Fn dom iEdg (G)$
11	7 8 10	3syl	$⊢ G \in UMGraph \to iEdg (G) Fn dom iEdg (G)$
12	11	adantl	$⊢ (G \in ConnGraph \land G \in UMGraph) \to iEdg (G) Fn dom iEdg (G)$
13	12	adantr	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to iEdg (G) Fn dom iEdg (G)$
14		simpl	$⊢ (G \in ConnGraph \land G \in UMGraph) \to G \in ConnGraph$
15	14	adantr	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to G \in ConnGraph$
16		simpl	$⊢ (N \in V \land 1 < \|V\|) \to N \in V$
17	16	adantl	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to N \in V$
18		simprr	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to 1 < \|V\|$
19	1 2	conngrv2edg	$⊢ (G \in ConnGraph \land N \in V \land 1 < \|V\|) \to \exists e \in ran iEdg (G) N \in e$
20	15 17 18 19	syl3anc	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to \exists e \in ran iEdg (G) N \in e$
21		eleq2	$⊢ e = iEdg (G) (x) \to (N \in e \leftrightarrow N \in iEdg (G) (x))$
22	21	rexrn	$⊢ iEdg (G) Fn dom iEdg (G) \to (\exists e \in ran iEdg (G) N \in e \leftrightarrow \exists x \in dom iEdg (G) N \in iEdg (G) (x))$
23	22	biimpd	$⊢ iEdg (G) Fn dom iEdg (G) \to (\exists e \in ran iEdg (G) N \in e \to \exists x \in dom iEdg (G) N \in iEdg (G) (x))$
24	13 20 23	sylc	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to \exists x \in dom iEdg (G) N \in iEdg (G) (x)$
25		dfrex2	$⊢ \exists x \in dom iEdg (G) N \in iEdg (G) (x) \leftrightarrow \neg \forall x \in dom iEdg (G) \neg N \in iEdg (G) (x)$
26	24 25	sylib	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to \neg \forall x \in dom iEdg (G) \neg N \in iEdg (G) (x)$
27		fvex	$⊢ iEdg (G) \in V$
28	27	dmex	$⊢ dom iEdg (G) \in V$
29	28	a1i	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to dom iEdg (G) \in V$
30		rabexg	$⊢ dom iEdg (G) \in V \to \{x \in dom iEdg (G) \| N \in iEdg (G) (x)\} \in V$
31		hasheq0	$⊢ \{x \in dom iEdg (G) \| N \in iEdg (G) (x)\} \in V \to (\|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\| = 0 \leftrightarrow \{x \in dom iEdg (G) \| N \in iEdg (G) (x)\} = \emptyset)$
32	29 30 31	3syl	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to (\|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\| = 0 \leftrightarrow \{x \in dom iEdg (G) \| N \in iEdg (G) (x)\} = \emptyset)$
33		rabeq0	$⊢ \{x \in dom iEdg (G) \| N \in iEdg (G) (x)\} = \emptyset \leftrightarrow \forall x \in dom iEdg (G) \neg N \in iEdg (G) (x)$
34	32 33	bitrdi	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to (\|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\| = 0 \leftrightarrow \forall x \in dom iEdg (G) \neg N \in iEdg (G) (x))$
35	34	necon3abid	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to (\|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\| \neq 0 \leftrightarrow \neg \forall x \in dom iEdg (G) \neg N \in iEdg (G) (x))$
36	26 35	mpbird	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to \|\{x \in dom iEdg (G) \| N \in iEdg (G) (x)\}\| \neq 0$
37	6 36	eqnetrd	$⊢ ((G \in ConnGraph \land G \in UMGraph) \land (N \in V \land 1 < \|V\|)) \to VtxDeg (G) (N) \neq 0$

Metamath Proof Explorer

Theorem vdn0conngrumgrv2

Proof